diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.mli b/src/plugins/e-acsl/src/code_generator/smart_exp.mli index b2a5e5b03f29073062d98a708adebc7a1548e7a1..2cffdd27908b6b7c5d8ec78a4c37ea4da8a37a2a 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_exp.mli +++ b/src/plugins/e-acsl/src/code_generator/smart_exp.mli @@ -47,8 +47,7 @@ val null: loc:location -> exp (** [null ~loc] creates an expression to represent the NULL pointer. *) val mem: loc:location -> varinfo -> exp -(** [mem ~loc v] creates an expression to represent the array access to the - first location of v *) +(** [mem ~loc v] creates a Mem expression with an explicit index of 0 *) (* Local Variables: compile-command: "make -C ../../../../.."