From aeabf5cd2c5a03c40768ef4edb14fcd1bbb4be9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Wed, 1 Sep 2021 17:07:18 +0200 Subject: [PATCH] [Eva] Adds an mli file for mark_noresults. --- src/plugins/value/utils/mark_noresults.mli | 27 ++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 src/plugins/value/utils/mark_noresults.mli diff --git a/src/plugins/value/utils/mark_noresults.mli b/src/plugins/value/utils/mark_noresults.mli new file mode 100644 index 00000000000..1fc95767ea9 --- /dev/null +++ b/src/plugins/value/utils/mark_noresults.mli @@ -0,0 +1,27 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2021 *) +(* 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). *) +(* *) +(**************************************************************************) + +(** Are the states of the function analysis saved? *) +val should_memorize_function: Cil_types.fundec -> bool + +(** Signal that some analysis results are not stored. *) +val no_memoization_enabled: unit -> bool -- GitLab