From 18276231d2ed0f3ac9a7a0034631f7c7525553b9 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 10 Dec 2015 14:38:38 +0100
Subject: [PATCH] [demo] improved + fix wrt kernel changes
---
src/plugins/e-acsl/demo/run_demo.sh | 4 +++-
src/plugins/e-acsl/demo/script.ml | 4 ++--
2 files changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/demo/run_demo.sh b/src/plugins/e-acsl/demo/run_demo.sh
index f110b94f001..38692596d29 100755
--- a/src/plugins/e-acsl/demo/run_demo.sh
+++ b/src/plugins/e-acsl/demo/run_demo.sh
@@ -2,6 +2,8 @@
E_ACSL_LIB=`frama-c -print-share-path`/e-acsl
-gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o ./demo pow.c $E_ACSL_LIB/e_acsl.c $E_ACSL_LIB/memory_model/e_acsl_bittree.c $E_ACSL_LIB/memory_model/e_acsl_mmodel.c res_demo.c
+gcc -c pow.c
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o ./demo pow.o $E_ACSL_LIB/e_acsl.c $E_ACSL_LIB/memory_model/e_acsl_bittree.c $E_ACSL_LIB/memory_model/e_acsl_mmodel.c res_demo.c
./demo
diff --git a/src/plugins/e-acsl/demo/script.ml b/src/plugins/e-acsl/demo/script.ml
index 2c078362659..d5ab61043e1 100644
--- a/src/plugins/e-acsl/demo/script.ml
+++ b/src/plugins/e-acsl/demo/script.ml
@@ -15,7 +15,7 @@ end)
(* ************************************************************************** *)
module Fct_name =
- EmptyString
+ Empty_string
(struct
let option_name = "-ppt-fct"
let help = "Name of the function in which the property is defined"
@@ -23,7 +23,7 @@ module Fct_name =
end)
module Ppt_name =
- EmptyString
+ Empty_string
(struct
let option_name = "-ppt-name"
let help = "Name of the property (assertion, ...)"
--
GitLab