From 4e02c251d8e3310eafaef5c8c8198c4eb8c3ec29 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 9 Feb 2023 14:29:01 +0100
Subject: [PATCH] [doc] more ACSL keywords
---
doc/frama-c-book.cls | 18 ++++++++++--------
1 file changed, 10 insertions(+), 8 deletions(-)
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index e8425770b1f..babfa353e3c 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]{//}
--
GitLab