diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls index e8425770b1fa148bb7e797121a09876eaeab66a9..babfa353e3c311bb2d94ead3ff5783f5c675c583 100644 --- a/doc/frama-c-book.cls +++ b/doc/frama-c-book.cls @@ -502,14 +502,16 @@ classoffset=1, morekeywords={admit,allocates,assert,assigns,assumes,axiom,axiomatic,behavior, behaviors,boolean,breaks,calls,check,complete,continues,data,decreases,disjoint, - ensures,exits,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop, - model,predicate,reads,real,requires,sizeof,strong,struct,terminates, - %returns, - type,union,variant - Here,LoopCurrent,LoopEntry,Pre,Post,Old, - \\at,\\allocable,\\base_addr,\\block_length,\\exists,\\false,\\forall, - \\freeable,\\fresh,\\from,\\initialized,\\nothing,\\numof,\\object_pointer, - \\offset,\\old,\\result,\\separated,\\sum,\\true,\\valid,\\valid_read}, + ensures,exits,frees,ghost,global,import,inductive,integer,invariant,lemma, + logic,loop,model,module,predicate,reads,real,requires,sizeof,strong,struct, + terminates,returns,type,union,variant, + Here,LoopCurrent,LoopEntry,Pre,Post,Old, + \\Cons,\\Down,\\NearestAway,\\NearestEven,\\Nil,\\ToZero,\\Up, + \\at,\\allocable,\\allocation,\\automatic,\\base_addr,\\block_length,\\dangling, + \\dynamic,\\exists,\\exit_status,\\false,\\forall,\\freeable,\\fresh,\\from, + \\in,\\initialized,\\lambda,\\let,\\list,\\match,\\nothing,\\null,\\numof, + \\object_pointer,\\offset,\\old,\\register,\\result,\\separated,\\static, + \\sum,\\true,\\unallocated,\\valid,\\valid_function,\\valid_read,\\with}, classoffset=0, alsoletter={\\}, morecomment=[l]{//}