Index: doc/refrat/refrat.tex =================================================================== --- doc/refrat/refrat.tex (revision a7528832a046957eb3c40dcea393f8024b8400a5) +++ doc/refrat/refrat.tex (revision 53ba273db2dfa4a4d251429b05f17a6400ed7f1e) @@ -1,2 +1,18 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- Mode: Latex -*- %%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% +%% Cforall Version 1.0.0 Copyright (C) 2016 University of Waterloo +%% +%% The contents of this file are covered under the licence agreement in the +%% file "LICENCE" distributed with Cforall. +%% +%% refrat.tex -- +%% +%% Author : Peter A. Buhr +%% Created On : Wed Apr 6 14:52:25 2016 +%% Last Modified By : Peter A. Buhr +%% Last Modified On : Wed Apr 6 21:57:27 2016 +%% Update Count : 2 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % requires tex packages: texlive-base texlive-latex-base tex-common texlive-humanities texlive-latex-extra texlive-fonts-recommended @@ -5,5 +21,4 @@ % Latex packages used in the document. - \usepackage{fullpage,times} \usepackage{xspace} @@ -23,5 +38,5 @@ % Names used in the document. -\newcommand{\CFA}{C$\forall$\xspace} % set language symbolic name +\newcommand{\CFA}{C$\mathbf\forall$\xspace} % set language symbolic name \newcommand{\CFL}{Cforall\xspace} % set language text name \newcommand{\CC}{C\kern-.1em\hbox{+\kern-.25em+}\xspace} % CC symbolic name @@ -151,7 +166,8 @@ % CFA based on ANSI C \lstdefinelanguage{CFA}[ANSI]{C}% -{morekeywords={asm,_Alignas,_Alignof,_At,_Atomic,_Bool,catch,catchResume,choose,_Complex,trait,disable,dtype,enable, - fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,lvalue,_Noreturn,otype,restrict,_Static_assert, - _Thread_local,throw,throwResume,try,}, +{morekeywords={_Alignas,_Alignof,__alignof,__alignof__,asm,__asm,__asm__,_At,_Atomic,__attribute,__attribute__,auto, + _Bool,catch,catchResume,choose,_Complex,__complex,__complex__,__const,__const__,disable,dtype,enable,__extension__, + fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,__label__,lvalue,_Noreturn,otype,restrict,_Static_assert, + _Thread_local,throw,throwResume,trait,try,typeof,__typeof,__typeof__,}, }% @@ -163,7 +179,10 @@ xleftmargin=\parindent, escapechar=@, +mathescape=true, keepspaces=true, showstringspaces=false, showlines=true, +aboveskip=6pt, +belowskip=4pt, }% @@ -171,9 +190,12 @@ % replace/adjust listings characters that look bad in sanserif \lst@CCPutMacro -\lst@ProcessOther{"2D}{\lst@ttfamily{-{}}{{\ttfamily\upshape -}}} % replace minus +\lst@ProcessOther{"22}{\lst@ttfamily{"}{\raisebox{0.3ex}{\ttfamily\upshape "}}} % replace double quote +\lst@ProcessOther{"27}{\lst@ttfamily{'}{\raisebox{0.3ex}{\ttfamily\upshape '\hspace*{-2pt}}}} % replace single quote +\lst@ProcessOther{"2D}{\lst@ttfamily{-}{\ttfamily\upshape -}} % replace minus \lst@ProcessOther{"3C}{\lst@ttfamily{<}{\texttt{<}}} % replace less than \lst@ProcessOther{"3E}{\lst@ttfamily{<}{\texttt{>}}} % replace greater than \lst@ProcessOther{"5E}{\raisebox{0.4ex}{$\scriptstyle\land\,$}} % replace circumflex -\lst@ProcessLetter{"5F}{\lst@ttfamily{\char95}{{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}}} % replace underscore +\lst@ProcessOther{"5F}{\lst@ttfamily{\char95}{{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}}} % replace underscore +\lst@ProcessOther{"60}{\lst@ttfamily{`}{\raisebox{0.3ex}{\ttfamily\upshape \hspace*{-2pt}`}}} % replace backquote \lst@ProcessOther{"7E}{\raisebox{0.3ex}{$\scriptstyle\sim\,$}} % replace tilde %\lst@ProcessOther{"7E}{\raisebox{-.4ex}[1ex][0pt]{\textasciitilde}} % lower tilde @@ -3843,17 +3865,17 @@ ``\lstinline$Safe_pointer$ acts like a pointer to \lstinline$int$''. \begin{lstlisting} -trait ptr_to( type P | pointer( P ), otype T ) {@\impl{ptr_to}@@\use{pointer}@ +trait ptr_to( otype P | pointer( P ), otype T ) {@\impl{ptr_to}@@\use{pointer}@ lvalue T *?( P ); lvalue T ?[?]( P, long int ); }; -trait ptr_to_const( type P | pointer( P ), otype T ) {@\impl{ptr_to_const}@ +trait ptr_to_const( otype P | pointer( P ), otype T ) {@\impl{ptr_to_const}@ const lvalue T *?( P ); const lvalue T ?[?]( P, long int );@\use{pointer}@ }; -trait ptr_to_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_volatile}@ +trait ptr_to_volatile( otype P | pointer( P ), otype T ) }@\impl{ptr_to_volatile}@ volatile lvalue T *?( P ); volatile lvalue T ?[?]( P, long int );@\use{pointer}@ }; -trait ptr_to_const_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_const_volatile}@ +trait ptr_to_const_volatile( otype P | pointer( P ), otype T ) }@\impl{ptr_to_const_volatile}@ const volatile lvalue T *?( P );@\use{pointer}@ const volatile lvalue T ?[?]( P, long int ); @@ -3865,18 +3887,18 @@ ``\lstinline$ptr_to$'' specifications. \begin{lstlisting} -trait m_l_ptr_to( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to}@ otype T | ptr_to( P, T )@\use{ptr_to}@ { +trait m_l_ptr_to( otype P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to}@ otype T | ptr_to( P, T )@\use{ptr_to}@ { P ?=?( P *, T * ); T * ?=?( T **, P ); }; -trait m_l_ptr_to_const( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_const}@ otype T | ptr_to_const( P, T )@\use{ptr_to_const}@) { +trait m_l_ptr_to_const( otype P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_const}@ otype T | ptr_to_const( P, T )@\use{ptr_to_const}@) { P ?=?( P *, const T * ); const T * ?=?( const T **, P ); }; -trait m_l_ptr_to_volatile( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_volatile}@ otype T | ptr_to_volatile( P, T )) {@\use{ptr_to_volatile}@ +trait m_l_ptr_to_volatile( otype P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_volatile}@ otype T | ptr_to_volatile( P, T )) {@\use{ptr_to_volatile}@ P ?=?( P *, volatile T * ); volatile T * ?=?( volatile T **, P ); }; -trait m_l_ptr_to_const_volatile( type P | ptr_to_const_volatile( P ),@\use{ptr_to_const_volatile}@@\impl{m_l_ptr_to_const_volatile}@ - type T | m_l_ptr_to_volatile( P, T ) | m_l_ptr_to_const( P )) {@\use{m_l_ptr_to_const}@@\use{m_l_ptr_to_volatile}@ +trait m_l_ptr_to_const_volatile( otype P | ptr_to_const_volatile( P ),@\use{ptr_to_const_volatile}@@\impl{m_l_ptr_to_const_volatile}@ + otype T | m_l_ptr_to_volatile( P, T ) | m_l_ptr_to_const( P )) {@\use{m_l_ptr_to_const}@@\use{m_l_ptr_to_volatile}@ P ?=?( P *, const volatile T * ); const volatile T * ?=?( const volatile T **, P );