From 29f08b19a527cf1878b208d23c00023818b0a5e7 Mon Sep 17 00:00:00 2001 From: Thibaut <thibaut.benjamin@cea.fr> Date: Mon, 26 Jul 2021 10:18:37 +0200 Subject: [PATCH] [e-acsl] new files for processing quantifiers --- src/plugins/e-acsl/Makefile.in | 3 +- src/plugins/e-acsl/headers/header_spec.txt | 2 ++ .../e-acsl/src/analyses/bound_variables.ml | 33 +++++++++++++++++++ .../e-acsl/src/analyses/bound_variables.mli | 22 +++++++++++++ 4 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 src/plugins/e-acsl/src/analyses/bound_variables.ml create mode 100644 src/plugins/e-acsl/src/analyses/bound_variables.mli diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index bc2d25e3ede..d5d488ff22b 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -63,7 +63,8 @@ SRC_ANALYSES:= \ exit_points \ lscope \ interval \ - typing + typing \ + bound_variables SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES)) # code generator diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt index 7f24e72705c..f6e7a2458de 100644 --- a/src/plugins/e-acsl/headers/header_spec.txt +++ b/src/plugins/e-acsl/headers/header_spec.txt @@ -67,6 +67,8 @@ share/e-acsl/observation_model/e_acsl_observation_model.c: CEA_LGPL_OR_PROPRIETA share/e-acsl/observation_model/e_acsl_observation_model.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml new file mode 100644 index 00000000000..eeb8edc7e90 --- /dev/null +++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml @@ -0,0 +1,33 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +(** Module for preprocessing the quantified predicates. Predicates with + quantifiers are hard to translate, so we delegate some of the work to a + preprocessing phase. At the end of this phase, all the quantified predicates + should have an associated preprocessed form [vars * goal] where - [vars] is a + list of guarded variables in the right order - [goal] is the predicate under + the quantifications The guarded variables in the list [vars] are of type + [term * logic_var * term * predicate option], where a tuple [(t1,v,t2,p)] + indicates that v is a logic variable with the two guards t1 <= x < t2 and p + is an additional optional guard to intersect the first guard with the + provided type for the variable v *) + diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.mli b/src/plugins/e-acsl/src/analyses/bound_variables.mli new file mode 100644 index 00000000000..73faeaec2c0 --- /dev/null +++ b/src/plugins/e-acsl/src/analyses/bound_variables.mli @@ -0,0 +1,22 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + -- GitLab