diff --git a/src/plugins/value/utils/mark_noresults.mli b/src/plugins/value/utils/mark_noresults.mli new file mode 100644 index 0000000000000000000000000000000000000000..1fc95767ea9e6b6bb776f4ac229d15e57aebc168 --- /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