From c2451b67fa59deeb167434d1ea1accf7b24dc8a2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 25 Feb 2019 18:57:32 +0100
Subject: [PATCH] =?UTF-8?q?[devman]=20fixes=20example=20of=20ACSL=20extens?=
=?UTF-8?q?ion=20(and=20Makefile=20`check`=20rule=20=F0=9F=98=9E)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
doc/developer/Makefile | 2 +-
doc/developer/examples/acsl_extension.ml | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index ab52d0e4172..4ce9e948e29 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -49,7 +49,7 @@ else
-load-script ./examples/acsl_extension \
-load-script ./hello_world/hello_world.ml \
| tee check.log
- if grep -e "user error" check.log; then \
+ if grep -e "User Error" check.log; then \
echo "Examples script do not compile with current Frama-C."; \
echo "Please examine check.log and make appropriate changes"; \
exit 1; \
diff --git a/doc/developer/examples/acsl_extension.ml b/doc/developer/examples/acsl_extension.ml
index b4848615dd5..9c677e00200 100644
--- a/doc/developer/examples/acsl_extension.ml
+++ b/doc/developer/examples/acsl_extension.ml
@@ -14,4 +14,4 @@ let type_foo ~typing_context ~loc:_loc l =
in
Ext_terms res
-let () = Logic_typing.register_behavior_extension "foo" type_foo
+let () = Logic_typing.register_behavior_extension "foo" false type_foo
--
GitLab