\lstdefinelanguage[ACSL]{C}[ANSI]{C}%
   {morekeywords={requires,ensures,assigns,loop,invariant,variant,
      terminates,decreases,
      behavior,assumes,complete,disjoint,behaviors,
      \nothing,\result,\at,\valid,
      \max,\numof,\sum,\lambda,
      \null,\base_addr,\block_length,\offset,\allocation,
      \allocable,\freeable,\fresh,\valid,\valid_read,\separated,
      bool, boolean, integer, real, size_type, value_type,
      then, skip,
      logic,axiom,axiomatic,predicate,inductive,lemma},%
%    otherkeywords={/*@,*/},
%    otherkeywords={->},% TeX capacity exceeded, sorry [grouping levels=255].
    deletecomment=[s]{/*}{*/},%
    deletecomment=[l]//,% nonstandard
    comment=[l]/// ,% to avoid matching //@
%    morecomment=[s]{/* }{*/},%
    literate=%
{\\langle}{\ensuremath{\langle}}1%
{\\rangle}{\ensuremath{\rangle}}1%
{->}{\ensuremath{\rightarrow}~}2%
{==}{\ensuremath{\equiv}~}{2}%
{!=}{\ensuremath{\neq}~}{2}%
{<=}{\ensuremath{\leq}~}{2}%
{>=}{\ensuremath{\geq}~}{1}%
{&&}{\ensuremath{\ \wedge\ }}{2}%
{||}{\ensuremath{\ \vee\ }}{2}%
{==>}{\ensuremath{\ \Rightarrow\ }}{3}%
{<==>}{\ensuremath{\ \Leftrightarrow\ }}{4}%
%{\\nothing}{$\emptyset$}{1}%
{\\forall}{\ensuremath{\forall\ }}{2}%
{\\exists}{\ensuremath{\exists\ }}{2},%
%{\\lambda}{\ensuremath{\mathbf{\lambda}\ }}{2},%
   }[keywords,strings,directives]%

\def\lstShowTarget{\gdef\lsttarget##1{\textsf{##1}:}}