diff --git a/.Makefile.lint b/.Makefile.lint
index 0d06aec2a52cabd62013b44313fc1ec5de6f4143..5a4002feff4dae338f2f4e1b0ecce3417bb7c167 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -69,13 +69,10 @@ ML_LINT_KO+=src/kernel_services/ast_data/ast.mli
ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.ml
ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.mli
ML_LINT_KO+=src/kernel_services/ast_data/property_status.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.ml
-ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil_const.ml
ML_LINT_KO+=src/kernel_services/ast_queries/cil_const.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil_datatype.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil_state_builder.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/file.mli
ML_LINT_KO+=src/kernel_services/ast_queries/logic_const.mli
ML_LINT_KO+=src/kernel_services/ast_transformations/clone.ml
ML_LINT_KO+=src/kernel_services/ast_transformations/clone.mli
@@ -99,8 +96,6 @@ ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.ml
ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.mli
ML_LINT_KO+=src/kernel_services/visitors/cabsvisit.ml
ML_LINT_KO+=src/kernel_services/visitors/cabsvisit.mli
-ML_LINT_KO+=src/kernel_services/visitors/visitor.ml
-ML_LINT_KO+=src/kernel_services/visitors/visitor.mli
ML_LINT_KO+=src/libraries/datatype/datatype.ml
ML_LINT_KO+=src/libraries/datatype/datatype.mli
ML_LINT_KO+=src/libraries/datatype/descr.ml
@@ -189,7 +184,6 @@ ML_LINT_KO+=src/plugins/gui/analyses_manager.ml
ML_LINT_KO+=src/plugins/gui/book_manager.ml
ML_LINT_KO+=src/plugins/gui/book_manager.mli
ML_LINT_KO+=src/plugins/gui/design.mli
-ML_LINT_KO+=src/plugins/gui/filetree.mli
ML_LINT_KO+=src/plugins/gui/gtk_form.ml
ML_LINT_KO+=src/plugins/gui/gtk_form.mli
ML_LINT_KO+=src/plugins/gui/gui_printers.ml
@@ -233,8 +227,6 @@ ML_LINT_KO+=src/plugins/inout/register.ml
ML_LINT_KO+=src/plugins/loop_analysis/region_analysis.ml
ML_LINT_KO+=src/plugins/loop_analysis/region_analysis_stmt.ml
ML_LINT_KO+=src/plugins/metrics/metrics_acsl.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_base.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_base.mli
ML_LINT_KO+=src/plugins/metrics/metrics_cabs.ml
ML_LINT_KO+=src/plugins/metrics/metrics_cilast.mli
ML_LINT_KO+=src/plugins/metrics/metrics_coverage.ml
@@ -310,8 +302,6 @@ ML_LINT_KO+=src/plugins/studia/studia_gui.ml
ML_LINT_KO+=src/plugins/studia/studia_gui.mli
ML_LINT_KO+=src/plugins/users/users_register.ml
ML_LINT_KO+=src/plugins/value_types/cilE.mli
-ML_LINT_KO+=src/plugins/value_types/cvalue.ml
-ML_LINT_KO+=src/plugins/value_types/cvalue.mli
ML_LINT_KO+=src/plugins/value_types/function_Froms.ml
ML_LINT_KO+=src/plugins/value_types/function_Froms.mli
ML_LINT_KO+=src/plugins/value_types/inout_type.ml
diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
new file mode 100644
index 0000000000000000000000000000000000000000..01adddbfea9dcbf30f2828c8156e06303c77decf
--- /dev/null
+++ b/.git-blame-ignore-revs
@@ -0,0 +1 @@
+0fc9094d8a7133f76295955a661fc24f51d276fd
diff --git a/.gitlab/issue_templates/bug_report.md b/.gitlab/issue_templates/bug_report.md
index b01c0a798eea16182a8c10988dd03d4c870a5e32..62e77a15383c43c4c96ceec40c053eff506b9dd3 100644
--- a/.gitlab/issue_templates/bug_report.md
+++ b/.gitlab/issue_templates/bug_report.md
@@ -5,7 +5,8 @@ Please directly edit it inline to provide the required information.
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [ ] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
-- [ ] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
+- [ ] the issue has not yet been reported on our old
+ [BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
diff --git a/Changelog b/Changelog
index b0b83bfa839e30d961958ffa80ca0dd162f8c766..dc7daa37201d8521e45b0859656514ced7af7cb0 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,9 @@
Open Source Release <next-release>
##################################
+o Kernel [2020-11-27] Extract builtin-related functions from module Cil
+ to module Cil_builtins. Code can be updated using
+ `bin/migration_scripts/titanium2vanadium.sh`.
- Metrics [2020-10-27] Add json output in addition to text and html
###################################
diff --git a/Makefile b/Makefile
index e1ca59aa35eb257c0cb24bda1552537f7e364e54..9ba399bd7896b5a8cf2b6bbde0f1d5038c1ed411 100644
--- a/Makefile
+++ b/Makefile
@@ -317,7 +317,7 @@ DISTRIB_FILES:=\
opam/opam \
# Test files to be included in the distribution (without header checking).
-# Plug-ins should use PLUGIN_DISTRIB_TESTS to export their test files.
+# Plug-ins should use PLUGIN_DISTRIB_TESTS to export their test files.
DISTRIB_TESTS=$(shell git ls-files \
tests \
src/plugins/aorai/tests \
@@ -518,6 +518,7 @@ KERNEL_CMO=\
src/kernel_services/ast_queries/logic_const.cmo \
src/kernel_services/visitors/visitor_behavior.cmo \
src/kernel_services/ast_queries/cil.cmo \
+ src/kernel_services/ast_queries/cil_builtins.cmo \
src/kernel_internals/parsing/errorloc.cmo \
src/kernel_services/ast_printing/cil_printer.cmo \
src/kernel_services/ast_printing/cil_descriptive_printer.cmo \
@@ -2375,7 +2376,7 @@ DISTRIB_FILES += $(wildcard $(PLUGIN_DISTRIBUTED_LIST) \
DISTRIB_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST),\
$(DISTRIB_FILES))
-DISTRIB_TESTS += $(wildcard $(PLUGIN_DIST_TESTS_LIST))
+DISTRIB_TESTS += $(wildcard $(PLUGIN_DIST_TESTS_LIST))
SPECIFIED_OPEN_SOURCE:=$(OPEN_SOURCE)
diff --git a/bin/migration_scripts/titanium2vanadium.sh b/bin/migration_scripts/titanium2vanadium.sh
new file mode 100755
index 0000000000000000000000000000000000000000..0a7c48738ae6c256c0d06fc84f06aa28efe882f3
--- /dev/null
+++ b/bin/migration_scripts/titanium2vanadium.sh
@@ -0,0 +1,171 @@
+#!/bin/bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-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). #
+# #
+##########################################################################
+
+#
+# Converts a Frama-C plugin from Frama-C 22 Titanium to Frama-C 23 Vanadium,
+# on a best-efforts basis (no guarantee that the result is fully compatible).
+#
+# known missing features:
+# - doesn't follow symbolic links to directories
+
+DIR=
+
+# verbose on by default
+VERBOSE="v"
+
+# test once if sed supports -i (BSD/macOS does not)
+SED_HAS_I=$(sed --help 2>/dev/null | grep '\-i' 2>/dev/null)
+
+# [sedi file expressions] runs 'sed -i expressions' on the specified file;
+# if '-i' is not supported, creates a temporary file and overwrites the
+# original, like '-i' does.
+sedi ()
+{
+ file="$1"
+ shift
+ if [ -n "$SED_HAS_I" ]; then
+ sed -i "$@" "$file"
+ else
+ # option '-i' is not recognized by sed: use a tmp file
+ new_temp=`mktemp /tmp/frama-c.XXXXXXX` || exit 1
+ sed "$@" "$file" > "$new_temp"
+ mv -f "$new_temp" "$file"
+ fi
+}
+
+dirs ()
+{
+ if [ -z "$DIR" ]; then
+ DIR=.
+ fi
+}
+
+# [safe_goto d1 d2 cmd] goes to d1, runs cmd, and returns to d2
+safe_goto ()
+{
+ dir="$1"
+ cd "$dir"
+ $3
+ cd "$2"
+}
+
+goto ()
+{
+ if [ -d "$1" ]; then
+ safe_goto "$1" "$2" "$3"
+ else
+ echo "Directory '$1' does not exist. Omitted."
+ fi
+}
+
+process_file ()
+{
+ file="$1"
+ if [ "$VERBOSE" ]; then
+ echo "Processing file $file"
+ fi
+ sedi "$file" \
+ -e 's/Cil\.Frama_c_builtins/Cil_builtins.Frama_c_builtins/g' \
+ -e 's/Cil\.is_builtin/Cil_builtins.is_builtin/g' \
+ -e 's/Cil\.is_unused_builtin/Cil_builtins.is_unused_builtin/g' \
+ -e 's/Cil\.is_special_builtin/Cil_builtins.is_special_builtin/g' \
+ -e 's/Cil\.add_special_builtin/Cil_builtins.add_special_builtin/g' \
+ -e 's/Cil\.add_special_builtin_family/Cil_builtins.add_special_builtin_family/g' \
+ -e 's/Cil\.init_builtins/Cil_builtins.init_builtins/g' \
+ -e 's/Cil\.Builtin_functions/Cil_builtins.Builtin_functions/g' \
+ -e 's/Cil\.builtinLoc/Cil_builtins.builtinLoc/g'
+}
+
+apply_one_dir ()
+{
+ if [ "$VERBOSE" ]; then
+ echo "Processing directory `pwd`"
+ fi
+ for f in $(find . -maxdepth 1 -type f -name "*.ml*" 2> /dev/null); do
+ process_file "$f"
+ done
+}
+
+apply_recursively ()
+{
+ apply_one_dir
+ while IFS= read -r -d $'\0' d; do
+ if [ "$d" = "." ]; then
+ continue
+ fi
+ safe_goto "$d" .. apply_recursively
+ done < <(find . -maxdepth 1 -type d -print0)
+}
+
+applying_to_list ()
+{
+ dirs
+ tmpdir=`pwd`
+ for d in $DIR; do
+ goto "$d" "$tmpdir" "$1"
+ done
+}
+
+help ()
+{
+ echo "Usage: $0 [options | directories]
+
+Options are:
+ -r | --recursive Check subdirectories recursively
+ -h | --help Display help message
+ -q | --quiet Quiet mode (i.e. non-verbose mode)
+ -v | --verbose Verbose mode (default)"
+ exit 0
+}
+
+error ()
+{
+ echo "$1.
+Do \"$0 -h\" for help."
+ exit 1
+}
+
+FN="apply_one_dir"
+
+parse_arg ()
+{
+ case $1 in
+ -r | --recursive) FN="apply_recursively";;
+ -h | -help ) help; exit 0;;
+ -q | --quiet ) VERBOSE=;;
+ -v | --verbose ) VERBOSE="v";;
+ -* ) error "Invalid option $1";;
+ * ) DIR="$DIR $1";;
+ esac
+}
+
+cmd_line ()
+{
+ for s in "$@"; do
+ parse_arg "$s"
+ done
+ applying_to_list $FN
+}
+
+cmd_line "$@"
+exit 0
diff --git a/doc/pdg/main.tex b/doc/pdg/main.tex
index 3c36466ebbccfe3fbfc8290100bcd25276579c4c..ca47e607056375c04fe2cd5f00a980bdc09c3f60 100644
--- a/doc/pdg/main.tex
+++ b/doc/pdg/main.tex
@@ -14,7 +14,8 @@
\title{Documentation du greffon PDG}{Calcul de dépendances dans un programme C}
\author{Anne Pacalet et Patrick Baudin}
\begin{tabular}{l}
-CEA LIST, Laboratoire de Sûreté et Sécurité des Logiciels, Saclay, F-91191 \\
+ CEA-List, Université Paris-Saclay \\
+ Laboratoire de Sûreté et Sécurité des Logiciels \\
\end{tabular}
\vfill
\begin{flushleft}
diff --git a/doc/slicing/main.tex b/doc/slicing/main.tex
index a95e2a4163b83cb2eaa8a26b036775a612a1dc0c..84b6368ed1a84dba5be85e2d8a4dad3d82692fca 100644
--- a/doc/slicing/main.tex
+++ b/doc/slicing/main.tex
@@ -16,7 +16,8 @@
\title{Documentation du greffon Slicing}{Conception d'un outil de Slicing}
\author{Anne Pacalet et Patrick Baudin}
\begin{tabular}{l}
-CEA List, Laboratoire de Sûreté et Sécurité des Logiciels, Saclay, F-91191 \\
+ CEA-List, Université Paris-Saclay \\
+ Laboratoire de Sûreté et Sécurité des Logiciels \\
\end{tabular}
\vfill
\begin{flushleft}
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index ed8bc97009e08a81c67fdf22e9b27724a2f4a80f..d52363f4281bd136fe28d7872fbaf083cd1f9b7c 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -41,6 +41,7 @@ bin/migration_scripts/sodium2magnesium.sh: CEA_LGPL
bin/migration_scripts/sulfur2chlorine.sh: CEA_LGPL
bin/migration_scripts/chlorine2argon.sh: CEA_LGPL
bin/migration_scripts/potassium2calcium.sh: CEA_LGPL
+bin/migration_scripts/titanium2vanadium.sh: CEA_LGPL
bin/sed_get_binutils_version: .ignore
bin/sed_get_make_major: .ignore
bin/sed_get_make_minor: .ignore
@@ -541,6 +542,8 @@ src/kernel_services/ast_queries/ast_info.ml: CEA_LGPL
src/kernel_services/ast_queries/ast_info.mli: CEA_LGPL
src/kernel_services/ast_queries/cil.ml: CIL
src/kernel_services/ast_queries/cil.mli: CIL
+src/kernel_services/ast_queries/cil_builtins.ml: CIL
+src/kernel_services/ast_queries/cil_builtins.mli: CIL
src/kernel_services/ast_queries/cil_const.ml: CIL
src/kernel_services/ast_queries/cil_const.mli: CIL
src/kernel_services/ast_queries/cil_datatype.ml: CEA_LGPL
diff --git a/ivette/src/dome/src/main/menubar.ts b/ivette/src/dome/src/main/menubar.ts
index 292cfffe70f7b787086b66501026aefe504fc654..5ca2f7ed903e25445a82f67b147a64e0c08c913c 100644
--- a/ivette/src/dome/src/main/menubar.ts
+++ b/ivette/src/dome/src/main/menubar.ts
@@ -162,6 +162,16 @@ const editMenuItems: MenuSpec = [
accelerator: 'CmdOrCtrl+A',
role: 'selectAll',
},
+ Separator,
+ {
+ label: 'Find',
+ accelerator: 'CmdOrCtrl+F',
+ click: (
+ _item: Electron.MenuItem,
+ window: Electron.BrowserWindow,
+ _evt: Electron.KeyboardEvent,
+ ) => window.webContents.send('dome.ipc.find'),
+ },
];
// --------------------------------------------------------------------------
@@ -326,8 +336,13 @@ export function addMenuItem(custom: CustomMenuItemSpec) {
}
if (entry.spec) Object.assign(entry.spec, spec);
if (entry.item) Object.assign(entry.item, spec);
-
} else {
+ if (!spec.click && !spec.role)
+ spec.click = (
+ _item: Electron.MenuItem,
+ window: Electron.BrowserWindow,
+ _evt: Electron.KeyboardEvent,
+ ) => window.webContents.send('dome.ipc.menu.clicked', id);
customItems.set(id, { spec });
menuSpec.push(spec);
}
diff --git a/ivette/src/dome/src/renderer/controls/labels.tsx b/ivette/src/dome/src/renderer/controls/labels.tsx
index aab6e501780f3478424ad3619c19552430ff8bb7..a9250344cc81c7cf3a1f2e374fc259e711c3df64 100644
--- a/ivette/src/dome/src/renderer/controls/labels.tsx
+++ b/ivette/src/dome/src/renderer/controls/labels.tsx
@@ -16,6 +16,7 @@ import './style.css';
// --- Generic Label
// --------------------------------------------------------------------------
+/** Labels support fowarding refs to their inner [<label/>] element. */
export interface LabelProps {
/** Text of the label. Prepend to other children elements. */
label?: string;
@@ -31,9 +32,13 @@ export interface LabelProps {
display?: boolean;
/** Additional content of the `<label/>` element. */
children?: React.ReactNode;
+ /** Click event callback. */
+ onClick?: (evt: React.MouseEvent) => void;
+ /** Right-click event callback. */
+ onContextMenu?: (evt: React.MouseEvent) => void;
}
-const makeLabel = (className: string, props: LabelProps) => {
+const makeLabel = (className: string) => (props: LabelProps, ref: any) => {
const { display = true } = props;
const allClasses = classes(
className,
@@ -42,9 +47,12 @@ const makeLabel = (className: string, props: LabelProps) => {
);
return (
<label
+ ref={ref}
className={allClasses}
title={props.title}
style={props.style}
+ onClick={props.onClick}
+ onContextMenu={props.onContextMenu}
>
{props.icon && <Icon title={props.title} id={props.icon} />}
{props.label}
@@ -68,18 +76,18 @@ const TCODE = 'dome-xLabel dome-text-code';
// --------------------------------------------------------------------------
/** Simple labels. */
-export const Label = (props: LabelProps) => makeLabel(LABEL, props);
+export const Label = React.forwardRef(makeLabel(LABEL));
/** Title and headings. */
-export const Title = (props: LabelProps) => makeLabel(TITLE, props);
+export const Title = React.forwardRef(makeLabel(TITLE));
/** Description, textbook content. */
-export const Descr = (props: LabelProps) => makeLabel(DESCR, props);
+export const Descr = React.forwardRef(makeLabel(DESCR));
/** Selectable textual information. */
-export const Data = (props: LabelProps) => makeLabel(TDATA, props);
+export const Data = React.forwardRef(makeLabel(TDATA));
/** Selectable inlined source-code content. */
-export const Code = (props: LabelProps) => makeLabel(TCODE, props);
+export const Code = React.forwardRef(makeLabel(TCODE));
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/src/renderer/dome.tsx b/ivette/src/dome/src/renderer/dome.tsx
index dda75f7467022882903bab4e3ea0bd696440e2f0..b1e1d879afc1defc21759cf0ba17a932a7f41fca 100644
--- a/ivette/src/dome/src/renderer/dome.tsx
+++ b/ivette/src/dome/src/renderer/dome.tsx
@@ -98,13 +98,17 @@ export class Event<A = void> {
}
+/** Custom React Hook on event. */
export function useEvent<A>(
- evt: Event<A>,
+ evt: undefined | null | Event<A>,
callback: (arg: A) => void,
) {
return React.useEffect(() => {
- evt.on(callback);
- return () => evt.off(callback);
+ if (evt) {
+ evt.on(callback);
+ return () => evt.off(callback);
+ }
+ return undefined;
});
}
@@ -126,9 +130,14 @@ export const update = new Event('dome.update');
It is emitted when the entire window is reloaded.
*/
export const reload = new Event('dome.reload');
-
ipcRenderer.on('dome.ipc.reload', () => reload.emit());
+/**
+ Dome « Find » event. Trigered by [Cmd+F] and [Edit > Find] menu.
+ */
+export const find = new Event('dome.find');
+ipcRenderer.on('dome.ipc.find', () => find.emit());
+
/** Command-line arguments event handler. */
export function onCommand(
job: (argv: string[], workingDir: string) => void,
diff --git a/ivette/src/dome/src/renderer/frame/style.css b/ivette/src/dome/src/renderer/frame/style.css
index b022fbc981f08628459bfc9df3d0043611f62dd0..5ec0dd8eba070447366ccea4defb7cf1b1577ac5 100644
--- a/ivette/src/dome/src/renderer/frame/style.css
+++ b/ivette/src/dome/src/renderer/frame/style.css
@@ -271,7 +271,7 @@
/* Layout */
-.dome-xToolBar-Control {
+.dome-xToolBar-control {
flex: 0 0 auto ;
height: 21px ;
margin: 6px 5px 6px 5px ;
@@ -282,72 +282,72 @@
outline: none ;
}
-.dome-xToolBar-Control svg {
+.dome-xToolBar-control svg {
height: 10px ;
position: relative ;
}
-.dome-xToolBar-Control svg + label {
+.dome-xToolBar-control svg + label {
margin-left: 4px ;
}
/* Background */
-.dome-window-active .dome-xToolBar-Control {
+.dome-window-active .dome-xToolBar-control {
background-image: linear-gradient(to bottom, #e8e8e8 0, #f1f1f1 100%);
}
-.dome-window-active .dome-xToolBar-Control:hover:not(:disabled) {
+.dome-window-active .dome-xToolBar-control:hover:not(:disabled) {
background-color: #ffffff ;
background-image: none ;
}
-.dome-window-active .dome-xToolBar-Control.dome-xToolBar-positive:not(:disabled) {
+.dome-window-active .dome-xToolBar-control.dome-xToolBar-positive:not(:disabled) {
background-image: linear-gradient(to bottom, #34ff52 0%, #48fd64 100%);
}
-.dome-window-active .dome-xToolBar-Control.dome-xToolBar-positive:hover:not(:disabled) {
+.dome-window-active .dome-xToolBar-control.dome-xToolBar-positive:hover:not(:disabled) {
background-color: #00ff00 ;
background-image: none ;
}
-.dome-window-active .dome-xToolBar-Control.dome-xToolBar-negative:not(:disabled) {
+.dome-window-active .dome-xToolBar-control.dome-xToolBar-negative:not(:disabled) {
color: #ccc ;
fill: #ccc ;
background-image: linear-gradient(to bottom, #ec453e 0%, #ff4c47 100%);
}
-.dome-window-active .dome-xToolBar-Control.dome-xToolBar-negative:hover:not(:disabled) {
+.dome-window-active .dome-xToolBar-control.dome-xToolBar-negative:hover:not(:disabled) {
background-color: red ;
background-image: none ;
}
-.dome-window-active .dome-xToolBar-Control.dome-xToolBar-warning:not(:disabled) {
+.dome-window-active .dome-xToolBar-control.dome-xToolBar-warning:not(:disabled) {
background-image: linear-gradient(to bottom, #fece72 0%, #fcaa0e 100%);
}
-.dome-window-active .dome-xToolBar-Control.dome-xToolBar-warning:hover:not(:disabled) {
+.dome-window-active .dome-xToolBar-control.dome-xToolBar-warning:hover:not(:disabled) {
background-color: orange ;
background-image: none ;
}
-.dome-window-active .dome-xToolBar-Control.dome-xToolBar-cancel:not(:disabled) {
+.dome-window-active .dome-xToolBar-control.dome-xToolBar-cancel:not(:disabled) {
background-color: #c2c0c2 ;
background-image: none ;
}
-.dome-window-active .dome-xToolBar-Control.dome-xToolBar-cancel:hover:not(:disabled) {
+.dome-window-active .dome-xToolBar-control.dome-xToolBar-cancel:hover:not(:disabled) {
background-image: linear-gradient(to bottom, #e8e8e8 0, #f1f1f1 100%);
}
-.dome-window-inactive .dome-xToolBar-Control {
+.dome-window-inactive .dome-xToolBar-control {
box-shadow: none ;
background-image: none ;
}
/* Activated */
-.dome-window-active .dome-xToolBar-Control:active:not(:disabled) {
+.dome-window-active .dome-xToolBar-control:active:not(:disabled) {
fill: #ddd ;
color: #ddd ;
background-color: gray ;
@@ -356,21 +356,21 @@
/* Disabled */
-.dome-window-active .dome-xToolBar-Control:disabled {
+.dome-window-active .dome-xToolBar-control:disabled {
fill: #ccc ;
color: #ccc ;
box-shadow: none ;
border-color: #bbb ;
}
-.dome-window-inactive .dome-xToolBar-Control:disabled {
+.dome-window-inactive .dome-xToolBar-control:disabled {
fill: #ccc ;
color: #ccc ;
}
/* Selected */
-.dome-window-active .dome-xToolBar-Control.dome-selected {
+.dome-window-active .dome-xToolBar-control.dome-selected {
fill: #fff;
color: #fff;
border: 1px solid transparent ;
@@ -378,12 +378,12 @@
background-image: none ;
}
-.dome-window-active .dome-xToolBar-Control.dome-selected:hover {
+.dome-window-active .dome-xToolBar-control.dome-selected:hover {
background-color: #888 ;
background-image: none ;
}
-.dome-window-inactive .dome-xToolBar-Control.dome-selected {
+.dome-window-inactive .dome-xToolBar-control.dome-selected {
fill: #eee;
color: #eee;
background-color: #ccc ;
@@ -391,14 +391,14 @@
/* Selected & Disabled */
-.dome-window-active .dome-xToolBar-Control.dome-selected:disabled {
+.dome-window-active .dome-xToolBar-control.dome-selected:disabled {
fill: #ccc ;
color: #ccc ;
border: 1px solid #bbb ;
background-color: #eee ;
}
-.dome-window-inactive .dome-xToolBar-Control.dome-selected:disabled {
+.dome-window-inactive .dome-xToolBar-control.dome-selected:disabled {
fill: #ccc ;
color: #ccc ;
border-color: #ddd ;
@@ -409,33 +409,107 @@
/* --- Styling ToolBar Button Group --- */
/* -------------------------------------------------------------------------- */
-.dome-xToolBar-Group {
+.dome-xToolBar-group {
display: flex ;
flex-direction: row ;
flex-wrap: nowrap ;
margin: 6px 5px 6px 5px ;
}
-.dome-xToolBar-Group .dome-xToolBar-Control {
+.dome-xToolBar-group .dome-xToolBar-control {
margin: 0 ;
}
-.dome-xToolBar-Group .dome-xToolBar-Control:not(:first-child) {
+.dome-xToolBar-group .dome-xToolBar-control:not(:first-child) {
border-left: 0 ;
}
-.dome-xToolBar-Group > .dome-xToolBar-Control:first-child {
+.dome-xToolBar-group > .dome-xToolBar-control:first-child {
border-top-right-radius: 0 ;
border-bottom-right-radius: 0 ;
}
-.dome-xToolBar-Group > .dome-xToolBar-Control:last-child {
+.dome-xToolBar-group > .dome-xToolBar-control:last-child {
border-top-left-radius: 0 ;
border-bottom-left-radius: 0 ;
}
-.dome-xToolBar-Group > .dome-xToolBar-Control:not(:first-child):not(:last-child) {
+.dome-xToolBar-group > .dome-xToolBar-control:not(:first-child):not(:last-child) {
border-radius: 0 ;
}
/* -------------------------------------------------------------------------- */
+/* --- Styling ToolBar Search Field --- */
+/* -------------------------------------------------------------------------- */
+
+.dome-xToolBar-control.dome-xToolBar-searchfield {
+ background-image: none ;
+ background-color: #eee ;
+ margin-top: 1px ;
+ padding-top: 1px ;
+ padding-left: 20px ;
+ border-radius: 12px ;
+ border-color: #aaa ;
+ width: 32px ;
+ transition: width 0.4s ease-in-out ;
+}
+
+.dome-window-inactive .dome-xToolBar-control.dome-xToolBar-searchfield {
+ background-color: #f6f6f6 ;
+ border-color: #ddd ;
+}
+
+.dome-xToolBar-searchfield:focus,
+.dome-xToolBar-searchfield:hover,
+.dome-xToolBar-searchicon:hover + .dome-xToolBar-searchfield
+{
+ width: 160px;
+}
+
+.dome-xToolBar-searchicon {
+ position: relative ;
+ overflow: visible ;
+ z-Index: +1;
+ height: 0px;
+ width: 0px;
+ top: 2px ;
+ left: 12px ;
+}
+
+.dome-window-inactive .dome-xToolBar-searchicon svg {
+ fill: #ccc ;
+}
+
+.dome-xToolBar-searchmenu {
+ position: relative ;
+ width: 162px ;
+ max-height: 120px ;
+ overflow-x: hidden ;
+ overflow-y: auto ;
+ left: -7px ;
+ top: 4px ;
+ padding: 0px ;
+ border: 1pt solid #aaa ;
+ background: #fff ;
+}
+
+.dome-xToolBar-searchitem {
+ display: block ;
+ width: 100% ;
+ margin-left: 0px ;
+ margin-right: 0px ;
+ padding-left: 4px ;
+ padding-right: 2px ;
+}
+
+.dome-xToolBar-searchitem:hover,
+.dome-xToolBar-searchindex
+{
+ background: lightblue !important;
+}
+
+.dome-xToolBar-searchitem:nth-child(even) {
+ background: #eef7f7;
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/dome/src/renderer/frame/toolbars.tsx b/ivette/src/dome/src/renderer/frame/toolbars.tsx
index 7ab35c1fedb18f1263b593d3e65fc1aa33c1a6f8..93d5c78ccc323d1ed613fd8350d8466248e5accf 100644
--- a/ivette/src/dome/src/renderer/frame/toolbars.tsx
+++ b/ivette/src/dome/src/renderer/frame/toolbars.tsx
@@ -8,16 +8,13 @@
*/
import React from 'react';
+import { Event, useEvent, find } from 'dome';
+import { debounce } from 'lodash';
+import { SVG } from 'dome/controls/icons';
+import { Label } from 'dome/controls/labels';
import { classes } from 'dome/misc/utils';
-
import './style.css';
-// --------------------------------------------------------------------------
-// --- ToolBar Button
-// --------------------------------------------------------------------------
-
-import { SVG } from 'dome/controls/icons';
-
// --------------------------------------------------------------------------
// --- ToolBar Container
// --------------------------------------------------------------------------
@@ -70,8 +67,8 @@ export const Separator = () => (
</div>
);
-const SELECT = 'dome-xToolBar-Control dome-selected';
-const BUTTON = 'dome-xToolBar-Control dome-color-frame';
+const SELECT = 'dome-xToolBar-control dome-selected';
+const BUTTON = 'dome-xToolBar-control dome-color-frame';
const KIND = (kind: undefined | string) => (
kind ? ` dome-xToolBar-${kind}` : ''
);
@@ -165,7 +162,7 @@ export function ButtonGroup<A>(props: SelectionProps<A>) {
onClick: onChange,
};
return (
- <div className="dome-xToolBar-Group">
+ <div className="dome-xToolBar-group">
{React.Children.map(children, (elt) => React.cloneElement(
elt,
{ ...baseProps, ...elt.props },
@@ -192,7 +189,7 @@ export function Select(props: SelectionProps<string>) {
};
return (
<select
- className="dome-xToolBar-Control dome-color-frame"
+ className="dome-xToolBar-control dome-color-frame"
value={props.value}
disabled={disabled || !enabled}
onChange={callback}
@@ -203,3 +200,154 @@ export function Select(props: SelectionProps<string>) {
}
// --------------------------------------------------------------------------
+// --- SearchField
+// --------------------------------------------------------------------------
+
+const DEBOUNCED_SEARCH = 200;
+
+const scrollToRef = (r: undefined | HTMLLabelElement) => {
+ if (r) r.scrollIntoView({ block: 'nearest' });
+};
+
+export interface Hint<A> {
+ id: string | number;
+ icon?: string;
+ label: string | JSX.Element;
+ title?: string;
+ value: A;
+}
+
+export interface SearchFieldProps<A> {
+ /** Tooltip Text. */
+ title?: string;
+ /** Placeholder Text. */
+ placeholder?: string;
+ /** Provided search hints (with respect to last `onSearch()` callback). */
+ hints?: Hint<A>[];
+ /** Search callback. Triggered on Enter Key, Escape Key or Blur event. */
+ onSelect?: (pattern: string) => void;
+ /** Dynamic search callback. Triggered on key pressed (debounced). */
+ onSearch?: (pattern: string) => void;
+ /** Hint selection callback. */
+ onHint?: (hint: Hint<A>) => void;
+ /** Event that triggers a focus request (defaults to [[Dome.find]]). */
+ event?: null | Event<void>;
+}
+
+/**
+ Search Bar.
+ */
+export function SearchField<A = undefined>(props: SearchFieldProps<A>) {
+ const inputRef = React.useRef<HTMLInputElement | null>(null);
+ const blur = () => inputRef.current?.blur();
+ const focus = () => inputRef.current?.focus();
+ const [value, setValue] = React.useState('');
+ const [index, setIndex] = React.useState(-1);
+ const { onHint, onSelect, onSearch, hints = [] } = props;
+
+ // Find event trigger
+ useEvent(props.event ?? find, focus);
+
+ // Lookup trigger
+ const triggerLookup = React.useCallback(
+ debounce((pattern: string) => {
+ if (onSearch) onSearch(pattern);
+ }, DEBOUNCED_SEARCH),
+ [onSearch],
+ );
+
+ // Blur Event
+ const onBlur = () => {
+ setValue('');
+ setIndex(-1);
+ if (onSearch) onSearch('');
+ };
+
+ // Key Events
+ const onKey = (evt: React.KeyboardEvent) => {
+ switch (evt.key) {
+ case 'Escape':
+ blur();
+ break;
+ case 'Enter':
+ if (index >= 0 && index < hints.length) {
+ if (onHint) onHint(hints[index]);
+ } else if (onSelect) onSelect(value);
+ blur();
+ break;
+ case 'ArrowUp':
+ if (index < 0) setIndex(hints.length - 1);
+ if (index > 0) setIndex(index - 1);
+ break;
+ case 'ArrowDown':
+ if (index < 0 && 0 < hints.length) setIndex(0);
+ if (0 <= index && index < hints.length - 1) setIndex(index + 1);
+ break;
+ }
+ };
+
+ // Input Events
+ const onChange = (evt: React.ChangeEvent<HTMLInputElement>) => {
+ const newValue = evt.target.value;
+ triggerLookup(newValue);
+ setIndex(-1);
+ setValue(newValue);
+ };
+
+ // Render Suggestions
+ const suggestions = hints.map((h, k) => {
+ const selected = k === index || hints.length === 1;
+ const className = classes(
+ 'dome-xToolBar-searchitem',
+ selected && 'dome-xToolBar-searchindex',
+ );
+ return (
+ <Label
+ ref={selected ? scrollToRef : undefined}
+ key={h.id}
+ icon={h.icon}
+ title={h.title}
+ className={className}
+ onClick={() => {
+ if (onHint) onHint(h);
+ blur();
+ }}
+ >
+ {h.label}
+ </Label>
+ );
+ });
+ const haspopup =
+ inputRef.current === document.activeElement
+ && suggestions.length > 0;
+ const visibility = haspopup ? 'visible' : 'hidden';
+
+ // Render Component
+ return (
+ <>
+ <div className="dome-xToolBar-searchicon">
+ <SVG id="SEARCH" />
+ <div
+ style={{ visibility }}
+ className="dome-xToolBar-searchmenu"
+ onMouseDown={(event) => event.preventDefault()}
+ >
+ {suggestions}
+ </div>
+ </div>
+ <input
+ ref={inputRef}
+ type="search"
+ title={props.title}
+ value={value}
+ placeholder={props.placeholder}
+ className="dome-xToolBar-control dome-xToolBar-searchfield"
+ onKeyUp={onKey}
+ onChange={onChange}
+ onBlur={onBlur}
+ />
+ </>
+ );
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index b42cf0c033c5def430170b76f6b62841342310dd..8582d0b50059c08e706a4ab2498344040be99998 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -19,7 +19,7 @@ import * as Controller from './Controller';
import ASTview from './ASTview';
import ASTinfo from './ASTinfo';
-import Globals from './Globals';
+import Globals, { GlobalHint, useHints } from './Globals';
import Properties from './Properties';
import Locations from './Locations';
import Values from './Values';
@@ -61,6 +61,14 @@ export default (() => {
Dome.useFlipSettings('frama-c.sidebar.unfold', true);
const [viewbar, flipViewbar] =
Dome.useFlipSettings('frama-c.viewbar.unfold', true);
+ const [hints, onSearchHint] = useHints();
+ const [, setSelection] = States.useSelection();
+ const onGlobalHint = (h: GlobalHint) => {
+ setSelection({ location: h.value });
+ };
+ const onSelectHint = () => {
+ if (hints.length === 1) onGlobalHint(hints[0]);
+ };
return (
<Vfill>
@@ -74,6 +82,13 @@ export default (() => {
<Controller.Control />
<HistorySelectionControls />
<Toolbar.Filler />
+ <Toolbar.SearchField
+ placeholder="Search…"
+ hints={hints}
+ onSearch={onSearchHint}
+ onSelect={onSelectHint}
+ onHint={onGlobalHint}
+ />
<Toolbar.Button
icon="ITEMS.GRID"
title="Customize Main View"
diff --git a/ivette/src/renderer/Globals.tsx b/ivette/src/renderer/Globals.tsx
index e3671fcb6374c78f776c16b5373e5541b0cf0d5b..aa3951e2ef087a3cb13a9c7e8639ac24aa2b2c8b 100644
--- a/ivette/src/renderer/Globals.tsx
+++ b/ivette/src/renderer/Globals.tsx
@@ -4,6 +4,7 @@
import React from 'react';
import { Section, Item } from 'dome/frame/sidebars';
+import type { Hint } from 'dome/frame/toolbars';
import * as States from 'frama-c/states';
import { alpha } from 'dome/data/compare';
import { functions, functionsData } from 'frama-c/api/kernel/ast';
@@ -25,7 +26,35 @@ const defaultFilter =
};
// --------------------------------------------------------------------------
-// --- Globals Section
+// --- Global Search Hints
+// --------------------------------------------------------------------------
+
+export type GlobalHint = Hint<States.Location>;
+
+const makeHint = (fct: functionsData): GlobalHint => ({
+ id: fct.key,
+ label: fct.name,
+ title: fct.signature,
+ value: { function: fct.name },
+});
+
+export function useHints(): [GlobalHint[], (pattern: string) => void] {
+ const fcts = States.useSyncArray(functions).getArray();
+ const [hints, setHints] = React.useState<GlobalHint[]>([]);
+ const onSearch = (pattern: string) => {
+ if (pattern === '') setHints([]);
+ else {
+ const p = pattern.toLowerCase();
+ setHints(fcts.filter((fn) => (
+ 0 <= fn.name.toLowerCase().indexOf(p)
+ )).map(makeHint));
+ }
+ };
+ return [hints, onSearch];
+}
+
+// --------------------------------------------------------------------------
+// --- Globals Section(s)
// --------------------------------------------------------------------------
export default () => {
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 97149facc4480fa64e0fe5b1a7fc5a4023c944f4..89737980d9c4855cf01eed52d767aef811f418df 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -36,6 +36,7 @@ const DEFAULTS: { [key: string]: boolean } = {
'status.invalid_hyp': true,
'status.considered_valid': false,
'status.untried': false,
+ 'status.dead': false,
'status.inconsistent': true,
'kind.assert': true,
'kind.invariant': true,
@@ -95,24 +96,25 @@ function filterStatus(
) {
switch (status) {
case 'valid':
- case 'valid_but_dead':
return filter('status.valid');
case 'valid_under_hyp':
return filter('status.valid_hyp');
case 'invalid':
- case 'invalid_but_dead':
return filter('status.invalid');
case 'invalid_under_hyp':
return filter('status.invalid_hyp');
case 'inconsistent':
- return filter('inconsistent');
+ return filter('status.inconsistent');
case 'unknown':
- case 'unknown_but_dead':
return filter('status.unknown');
case 'considered_valid':
- return filter('considered_valid');
+ return filter('status.considered_valid');
case 'never_tried':
return filter('status.untried');
+ case 'valid_but_dead':
+ case 'unknown_but_dead':
+ case 'invalid_but_dead':
+ return filter('status.dead');
default:
return true;
}
@@ -135,6 +137,7 @@ function filterKind(
case 'reachable': return filter('kind.reachable');
case 'axiomatic': return filter('kind.axiomatic');
case 'loop_pragma': return filter('kind.pragma');
+ case 'assumes': return filter('kind.assumes');
default: return filter('kind.others');
}
}
@@ -284,12 +287,11 @@ const Reload = new Dome.Event('ivette.properties.reload');
interface SectionProps {
label: string;
- path: string;
children: React.ReactNode;
}
function Section(props: SectionProps) {
- const settings = `properties-section-${props.path}`;
+ const settings = `properties-section-${props.label}`;
return (
<Folder label={props.label} settings={settings}>
{props.children}
@@ -321,7 +323,7 @@ function PropertyFilter() {
return (
<Scroll>
<CheckField label="Current function" path="currentFunction" />
- <Section label="Status" path="status">
+ <Section label="Status">
<CheckField label="Valid" path="status.valid" />
<CheckField label="Valid under hyp." path="status.valid_hyp" />
<CheckField label="Unknown" path="status.unknown" />
@@ -329,9 +331,10 @@ function PropertyFilter() {
<CheckField label="Invalid under hyp." path="status.invalid_hyp" />
<CheckField label="Considered valid" path="status.considered_valid" />
<CheckField label="Untried" path="status.untried" />
+ <CheckField label="Dead" path="status.dead" />
<CheckField label="Inconsistent" path="status.inconsistent" />
</Section>
- <Section label="Property kind" path="kind">
+ <Section label="Property kind">
<CheckField label="Assertions" path="kind.assert" />
<CheckField label="Invariants" path="kind.invariant" />
<CheckField label="Variants" path="kind.variant" />
@@ -339,19 +342,20 @@ function PropertyFilter() {
<CheckField label="Postconditions" path="kind.ensures" />
<CheckField label="Instance" path="kind.instance" />
<CheckField label="Assigns clauses" path="kind.assigns" />
- <CheckField label="From clauses" path="kind.from" />
+ <CheckField label="From clauses" path="kind.froms" />
<CheckField label="Allocates" path="kind.allocates" />
<CheckField label="Behaviors" path="kind.behavior" />
<CheckField label="Reachables" path="kind.reachable" />
<CheckField label="Axiomatics" path="kind.axiomatic" />
<CheckField label="Pragma" path="kind.pragma" />
+ <CheckField label="Assumes" path="kind.assumes" />
<CheckField label="Others" path="kind.others" />
</Section>
- <Section label="Alarms" path="alarms">
+ <Section label="Alarms">
<CheckField label="Alarms" path="alarms.alarms" />
<CheckField label="Others" path="alarms.others" />
</Section>
- <Section label="Alarms kind" path="alarms">
+ <Section label="Alarms kind">
<CheckField label="Overflows" path="alarms.overflow" />
<CheckField label="Divisions by zero" path="alarms.division_by_zero" />
<CheckField label="Shifts" path="alarms.shift" />
diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk
index 0e4910e1acfeb82f018a68576adfdc200fdaa988..a1319e9756817f674bcc22cb0d64debcc23810d2 100644
--- a/share/analysis-scripts/analysis.mk
+++ b/share/analysis-scripts/analysis.mk
@@ -84,7 +84,7 @@ else
SED_UNBUFFERED:=sed --unbuffered
ifneq (,$(wildcard /usr/bin/time))
define time_with_output
- /usr/bin/time --format='user_time=%U\nmemory=%M' --output="$(1)"
+ /usr/bin/time -f 'user_time=%U\nmemory=%M' -o "$(1)"
endef
else
define time_with_output
@@ -143,7 +143,7 @@ clean-backups:
HR_TIMESTAMP := $(shell date +"%H:%M:%S %d/%m/%Y")# Human readable
DIR := $(dir $(lastword $(MAKEFILE_LIST)))
-SHELL := /bin/bash
+SHELL := $(shell which bash)
.SHELLFLAGS := -eu -o pipefail -c
.ONESHELL:
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index ed72df096223334ce385db07fc050376f49d21b6..07c314b9d8a8679b51f13c03973d15e36091395e 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/share/analysis-scripts/make_wrapper.py
@@ -32,6 +32,7 @@ import re
import subprocess
import sys
from functools import partial
+import tempfile
MIN_PYTHON = (3, 6) # for automatic Path conversions
if sys.version_info < MIN_PYTHON:
@@ -40,7 +41,7 @@ if sys.version_info < MIN_PYTHON:
parser = argparse.ArgumentParser(description="""
Builds the specified target, parsing the output to identify and recommend
actions in case of failure.""")
-parser.add_argument('--make-dir', metavar='DIR', default=".frama-c", nargs=1,
+parser.add_argument('--make-dir', metavar='DIR', default=".frama-c",
help='directory containing the makefile (default: .frama-c)')
(make_dir_arg, args) = parser.parse_known_args()
@@ -52,10 +53,19 @@ if not framac_bin:
sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)")
framac_script = f"{framac_bin}/frama-c-script"
-out = subprocess.Popen(['make', "-C", make_dir] + args,
- stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
-
-output = out.communicate()[0].decode('utf-8')
+output_lines = []
+cmd_list = ['make', "-C", make_dir] + args
+with subprocess.Popen(cmd_list,
+ stdout=subprocess.PIPE,
+ stderr=subprocess.PIPE) as proc:
+ while True:
+ line = proc.stdout.readline()
+ if line:
+ sys.stdout.buffer.write(line)
+ sys.stdout.flush()
+ output_lines.append(line.decode('utf-8'))
+ else:
+ break
re_missing_spec = re.compile("Neither code nor specification for function ([^,]+),")
re_recursive_call_start = re.compile("detected recursive call")
@@ -63,9 +73,8 @@ re_recursive_call_end = re.compile("Use -eva-ignore-recursive-calls to ignore")
tips = []
-lines = iter(output.splitlines())
+lines = iter(output_lines)
for line in lines:
- print(line)
match = re_missing_spec.search(line)
if match:
fname = match.group(1)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 6779c775ca22b68c9f130da4418f1565a2aeeeee..084eaf5880092742d59053497a923de2415ec520 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3217,7 +3217,7 @@ let setupBuiltin ?(force_keep=false) name ?spec (resTyp, args_or_argtypes, isva)
| None -> empty_funspec ()
| Some s -> s
in
- cabsPushGlobal (GFunDecl (funspec, v, Cil.builtinLoc));
+ cabsPushGlobal (GFunDecl (funspec, v, Cil_builtins.builtinLoc));
Cil.unsafeSetFormalsDecl v args;
if force_keep then
v.vattr <- Cil.addAttribute (Attr ("FC_BUILTIN",[])) v.vattr;
@@ -6665,7 +6665,7 @@ and doExp local_env
* functions alone*)
let isSpecialBuiltin =
match f''.enode with
- | Lval (Var fv, NoOffset) -> Cil.is_special_builtin fv.vname
+ | Lval (Var fv, NoOffset) -> Cil_builtins.is_special_builtin fv.vname
| _ -> false
in
let init_chunk = unspecified_chunk empty in
@@ -10310,7 +10310,7 @@ let convFile (path, f) =
Logic_env.prepare_tables ();
anonCompFieldNameId := 0;
Kernel.debug ~level:2 "Converting CABS->CIL" ;
- Cil.Builtin_functions.iter_sorted
+ Cil_builtins.Builtin_functions.iter_sorted
(fun name (resTyp, argTypes, isva) ->
ignore (setupBuiltin name (resTyp, ArgTypes argTypes, isva)));
let globalidx = ref 0 in
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index ce796a384de5e708b69737cf6fe54e232bf39452..6af1cadc349d690ab660527690bcc8720024b2ca 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -172,16 +172,17 @@ class visitor = object(self)
| { enode = Lval ( (Var vi), NoOffset ) } -> Some vi
| _ -> None
in
+ let is_ghost vi = vi.vghost || Ast_info.is_frama_c_builtin vi.vname in
let failed = match i with
| Call(_, fexp, _, _) ->
begin match call_varinfo fexp with
- | Some fct when not fct.vghost ->
+ | Some fct when not (is_ghost fct) ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| None ->
Error.function_pointer_call ~current:true () ; true
| _ -> false
end
- | Local_init(_, ConsInit(fct, _, _), _) when not fct.vghost ->
+ | Local_init(_, ConsInit(fct, _, _), _) when not (is_ghost fct) ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| _ -> false
in
diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml
index 60a89abe305204587f016ebca8b64c0d9f3411ad..24a664faad73c180f9e2b37ad3dc4e7597e41629 100644
--- a/src/kernel_services/analysis/destructors.ml
+++ b/src/kernel_services/analysis/destructors.ml
@@ -280,7 +280,8 @@ class vis flag = object(self)
end
let treat_one_function flag kf =
- if not (Cil.is_special_builtin (Kernel_function.get_name kf)) then begin
+ if not (Cil_builtins.is_special_builtin (Kernel_function.get_name kf))
+ then begin
let my_flag = ref false in
let vis = new vis my_flag in
ignore (Visitor.visitFramacKf vis kf);
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index cae5f59e1f52990ea1df0ee8aa9ecab4caddfe69..a88e444703a4b42a6e31ee16441763906e6bc61a 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -307,7 +307,7 @@ module Functions = struct
*)
(*Kernel.feedback "adding empty fun for %a"
Cil_datatype.Varinfo.pretty vi; *)
- if Cil.is_special_builtin v.vname then
+ if Cil_builtins.is_special_builtin v.vname then
add_declaration (empty_funspec ()) v v.vdecl
else
raise Not_found
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 869bad2794f51fab9519f3f07afd68e57c040442..37364ee028462571d6efdbf3c42cdd033663f577 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -120,7 +120,7 @@ let print_global g =
not (Cil.hasAttribute "fc_stdlib" attrs) || Kernel.PrintLibc.get()
in
let print_var v =
- not (Cil.is_unused_builtin v) ||
+ not (Cil_builtins.is_unused_builtin v) ||
Kernel.is_debug_key_enabled Kernel.dkey_print_builtins
in
match g with
@@ -1755,7 +1755,8 @@ class cil_printer () = object (self)
| GFunDecl (funspec, vi, l) ->
self#in_current_function vi;
self#opt_funspec fmt funspec;
- if not state.print_cil_as_is && Cil.Builtin_functions.mem vi.vname
+ if not state.print_cil_as_is &&
+ Cil_builtins.Builtin_functions.mem vi.vname
then begin
(* Compiler builtins need no prototypes. Just print them in
comments. *)
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 7735444cd57cef665b84d6588e260f1a8f2950bb..5627363cb3a88ca1dbaa65998d569e268284b5fc 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -143,7 +143,7 @@ class printer_with_annot () = object (self)
then begin
declared_globs <- Cil_datatype.Varinfo.Set.add vi declared_globs;
(* pretty prints the spec, but not for built-ins*)
- if not (Cil.Builtin_functions.mem vi.vname) then
+ if not (Cil_builtins.Builtin_functions.mem vi.vname) then
self#pretty_funspec fmt kf
end
with Not_found ->
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 5242bfbf931263cd07838ba48bb6512b112b532a..b283054819553df4d0046b32ef3c7e8774123ea9 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -34,36 +34,36 @@ let is_integral_const = function
let rec possible_value_of_integral_const = function
| CInt64 (i,_,_) -> Some i
| CEnum {eival = e} -> possible_value_of_integral_expr e
- | CChr c -> Some (Integer.of_int (Char.code c))
+ | CChr c -> Some (Integer.of_int (Char.code c))
(* This is against the ISO C norm! See Cil.charConstToInt *)
| _ -> None
and possible_value_of_integral_expr e =
match (stripInfo e).enode with
- | Const c -> possible_value_of_integral_const c
- | _ -> None
+ | Const c -> possible_value_of_integral_const c
+ | _ -> None
let value_of_integral_const c =
match possible_value_of_integral_const c with
- | None -> assert false
- | Some i -> i
+ | None -> assert false
+ | Some i -> i
let value_of_integral_expr e =
match possible_value_of_integral_expr e with
- | None -> assert false
- | Some i -> i
+ | None -> assert false
+ | Some i -> i
let constant_expr ~loc i = new_exp ~loc (Const(CInt64(i,IInt,None)))
let rec is_null_expr e = match (stripInfo e).enode with
| Const c when is_integral_const c ->
- Integer.equal (value_of_integral_const c) Integer.zero
+ Integer.equal (value_of_integral_const c) Integer.zero
| CastE(_,e) -> is_null_expr e
| _ -> false
let rec is_non_null_expr e = match (stripInfo e).enode with
| Const c when is_integral_const c ->
- not (Integer.equal (value_of_integral_const c) Integer.zero)
+ not (Integer.equal (value_of_integral_const c) Integer.zero)
| CastE(_,e) -> is_non_null_expr e
| _ -> false
@@ -84,24 +84,24 @@ let possible_value_of_integral_logic_const = function
let value_of_integral_logic_const c =
match possible_value_of_integral_logic_const c with
- | None -> assert false
- | Some i -> i
+ | None -> assert false
+ | Some i -> i
let possible_value_of_integral_term t =
match t.term_node with
- | TConst c -> possible_value_of_integral_logic_const c
- | _ -> None
+ | TConst c -> possible_value_of_integral_logic_const c
+ | _ -> None
let term_lvals_of_term t =
let l = ref [] in
ignore
(Cil.visitCilTerm
(object
- inherit nopCilVisitor
- method! vterm_lval lv =
- l := lv :: !l;
- DoChildren
- end)
+ inherit nopCilVisitor
+ method! vterm_lval lv =
+ l := lv :: !l;
+ DoChildren
+ end)
t);
!l
@@ -119,8 +119,8 @@ let behavior_postcondition b k =
let behavior_precondition b =
let assumes = behavior_assumes b in
- let requires = Logic_const.pands
- (List.rev_map Logic_const.pred_of_id_pred b.b_requires)
+ let requires = Logic_const.pands
+ (List.rev_map Logic_const.pred_of_id_pred b.b_requires)
in
Logic_const.pimplies (assumes,requires)
@@ -134,16 +134,18 @@ let get_named_bhv bhv_list name =
let get_named_bhv_assumes spec bhv_names =
let bhvs = match bhv_names with
- | [] -> (* no names ==> all named behaviors *)
- List.filter (fun b -> not (is_default_behavior b)) spec.spec_behavior
- | _ ->
- let rec get l = match l with [] -> []
- | name::tl ->
- match get_named_bhv spec.spec_behavior name with
- | None -> (* TODO: warn ? *) get tl
- | Some b -> b::(get tl)
- in
- get bhv_names
+ | [] -> (* no names ==> all named behaviors *)
+ List.filter (fun b -> not (is_default_behavior b)) spec.spec_behavior
+ | _ ->
+ let rec get l =
+ match l with
+ | [] -> []
+ | name::tl ->
+ match get_named_bhv spec.spec_behavior name with
+ | None -> (* TODO: warn ? *) get tl
+ | Some b -> b::(get tl)
+ in
+ get bhv_names
in
List.map behavior_assumes bhvs
@@ -151,7 +153,7 @@ let complete_behaviors spec bhv_names =
let bhv_assumes = get_named_bhv_assumes spec bhv_names in
Logic_const.pors bhv_assumes
-let disjoint_behaviors spec bhv_names =
+let disjoint_behaviors spec bhv_names =
let bhv_assumes = get_named_bhv_assumes spec bhv_names in
let mk_disj_bhv b1 b2 = (* ~ (b1 /\ b2) *)
let p = Logic_const.pands [b1; b2] in
@@ -161,62 +163,64 @@ let disjoint_behaviors spec bhv_names =
let lp = List.map (mk_disj_bhv b) lb in
Logic_const.pands (prop::lp)
in
- let rec do_list prop l = match l with [] -> prop
- | b::tl ->
- let prop = do_one_with_list prop b tl in
- do_list prop tl
- in
- do_list Logic_const.ptrue bhv_assumes
+ let rec do_list prop l =
+ match l with
+ | [] -> prop
+ | b::tl ->
+ let prop = do_one_with_list prop b tl in
+ do_list prop tl
+ in
+ do_list Logic_const.ptrue bhv_assumes
let merge_assigns_internal (get:'b -> assigns) (origin:'b -> string list)
(acc:(('a*(bool * string list))*int) option) (bhvs: 'b list) =
- let cmp_assigns acc b =
+ let cmp_assigns acc b =
let a' = get b in
- match acc,a' with
- | _, WritesAny -> acc
- | None, Writes l ->
- (* use the number of assigned terms as measure *)
- Some ((a',(false,origin b)),List.length l)
- | (Some((a,(w,orig)),n)), Writes l ->
- let w = (* warning is needed? *)
- w || (a != a' && a <> WritesAny)
- in (* use the number of assigned terms as measure *)
- let m = List.length l in
- if n<0 || m<n then Some((a',(w,origin b)),m) else Some((a,(w,orig)),n)
+ match acc,a' with
+ | _, WritesAny -> acc
+ | None, Writes l ->
+ (* use the number of assigned terms as measure *)
+ Some ((a',(false,origin b)),List.length l)
+ | (Some((a,(w,orig)),n)), Writes l ->
+ let w = (* warning is needed? *)
+ w || (a != a' && a <> WritesAny)
+ in (* use the number of assigned terms as measure *)
+ let m = List.length l in
+ if n<0 || m<n then Some((a',(w,origin b)),m) else Some((a,(w,orig)),n)
in List.fold_left (* find the smallest one *)
- cmp_assigns acc bhvs
+ cmp_assigns acc bhvs
(** Returns the assigns from complete behaviors and unguarded behaviors. *)
let merge_assigns_from_complete_bhvs ?warn ?(unguarded=true) bhvs complete_bhvs =
let merge_assigns_from_complete_bhvs bhv_names =
try (* For merging assigns of a "complete" set of behaviors *)
let behaviors = match bhv_names with
- (* Extract behaviors from their names. *)
- | [] -> (* All behaviors should be taken except the default behavior *)
- List.filter (fun b -> not (Cil.is_default_behavior b)) bhvs
- | _ -> (* Finds the corresponding behaviors from the set *)
- List.map
- (fun b_name ->
- List.find (fun b -> b.b_name = b_name) bhvs) bhv_names
+ (* Extract behaviors from their names. *)
+ | [] -> (* All behaviors should be taken except the default behavior *)
+ List.filter (fun b -> not (Cil.is_default_behavior b)) bhvs
+ | _ -> (* Finds the corresponding behaviors from the set *)
+ List.map
+ (fun b_name ->
+ List.find (fun b -> b.b_name = b_name) bhvs) bhv_names
in
- (* Merges the assigns of the complete behaviors.
- Once one of them as no assumes, that means the merge
- of the unguarded behavior did already the job *)
+ (* Merges the assigns of the complete behaviors.
+ Once one of them as no assumes, that means the merge
+ of the unguarded behavior did already the job *)
Writes
- (List.fold_left
- (fun acc b -> match b.b_assigns with
- | Writes l when b.b_assumes <> [] -> l @ acc
- | _ -> raise Not_found) [] behaviors)
- with Not_found ->
+ (List.fold_left
+ (fun acc b -> match b.b_assigns with
+ | Writes l when b.b_assumes <> [] -> l @ acc
+ | _ -> raise Not_found) [] behaviors)
+ with Not_found ->
(* One of these behaviors is not found or has no assumes *)
WritesAny
in
let acc =
if unguarded then (* Looks first at unguarded behaviors. *)
- let unguarded_bhvs = List.filter (fun b -> b.b_assumes = []) bhvs
- in merge_assigns_internal (* Chooses the smallest one *)
- (fun b -> b.b_assigns) (fun b -> [b.b_name])
- None unguarded_bhvs
+ let unguarded_bhvs = List.filter (fun b -> b.b_assumes = []) bhvs
+ in merge_assigns_internal (* Chooses the smallest one *)
+ (fun b -> b.b_assigns) (fun b -> [b.b_name])
+ None unguarded_bhvs
else None
in
let acc = match acc with
@@ -226,28 +230,28 @@ let merge_assigns_from_complete_bhvs ?warn ?(unguarded=true) bhvs complete_bhvs
| _ ->
(* Look at complete behaviors *)
merge_assigns_internal (* Chooses the smallest one *)
- merge_assigns_from_complete_bhvs
- (fun bhvnames -> bhvnames)
- acc
- complete_bhvs
- in
+ merge_assigns_from_complete_bhvs
+ (fun bhvnames -> bhvnames)
+ acc
+ complete_bhvs
+ in
match acc with
| None -> WritesAny (* No unguarded behavior -> assigns everything *)
| Some ((a,(w,orig)),_) -> (* The smallest one *)
- let warn = match warn with
+ let warn = match warn with
| None -> w
- | Some warn -> warn
- in
+ | Some warn -> warn
+ in
if warn then begin
- let orig =
- if orig = [] then List.map (fun b -> b.b_name) bhvs else orig
+ let orig =
+ if orig = [] then List.map (fun b -> b.b_name) bhvs else orig
in
Kernel.warning ~once:true ~current:true
- "keeping only assigns from behaviors: %a"
- (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) orig
+ "keeping only assigns from behaviors: %a"
+ (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) orig
end;
a
-
+
(** Returns the assigns from complete behaviors and unguarded behaviors. *)
let merge_assigns_from_spec ?warn (spec :funspec) =
merge_assigns_from_complete_bhvs
@@ -256,21 +260,21 @@ let merge_assigns_from_spec ?warn (spec :funspec) =
(** Returns the assigns of an unguarded behavior. *)
let merge_assigns ?warn (bhvs : funbehavior list) =
let unguarded_bhvs = List.filter (fun b -> b.b_assumes = []) bhvs in
- let acc = merge_assigns_internal
- (fun b -> b.b_assigns) (fun b -> [b.b_name])
- None unguarded_bhvs
+ let acc = merge_assigns_internal
+ (fun b -> b.b_assigns) (fun b -> [b.b_name])
+ None unguarded_bhvs
in
match acc with
| None -> WritesAny (* No unguarded behavior -> assigns everything *)
| Some((a,(w,orig)),_) -> (* The smallest one *)
- let warn = match warn with
+ let warn = match warn with
| None -> w
- | Some warn -> warn
- in
+ | Some warn -> warn
+ in
if warn then
Kernel.warning ~once:true ~current:true
- "keeping only assigns from behaviors: %a"
- (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) orig;
+ "keeping only assigns from behaviors: %a"
+ (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) orig;
a
let variable_term loc v =
@@ -291,7 +295,7 @@ let constant_term loc i =
let rec is_null_term t = match t.term_node with
| TConst c when is_integral_logic_const c ->
- Integer.equal (value_of_integral_logic_const c) Integer.zero
+ Integer.equal (value_of_integral_logic_const c) Integer.zero
| TCastE(_,t) -> is_null_term t
| _ -> false
@@ -321,9 +325,9 @@ module Function = struct
let formal_args called_vinfo = match called_vinfo.vtype with
| TFun (_,Some argl,_,_) ->
- argl
+ argl
| TFun _ ->
- []
+ []
| _ -> assert false
let is_formal v fundec =
@@ -394,18 +398,18 @@ let array_type ?length ?(attr=[]) ty = TArray(ty,length,empty_size_cache (),attr
let direct_array_size ty =
match unrollType ty with
- | TArray(_ty,Some size,_,_) -> value_of_integral_expr size
- | TArray(_ty,None,_,_) -> Integer.zero
- | _ -> assert false
+ | TArray(_ty,Some size,_,_) -> value_of_integral_expr size
+ | TArray(_ty,None,_,_) -> Integer.zero
+ | _ -> assert false
let rec array_size ty =
match unrollType ty with
- | TArray(elemty,Some _,_,_) ->
- if isArrayType elemty then
- Integer.mul (direct_array_size ty) (array_size elemty)
- else direct_array_size ty
- | TArray(_,None,_,_) -> Integer.zero
- | _ -> assert false
+ | TArray(elemty,Some _,_,_) ->
+ if isArrayType elemty then
+ Integer.mul (direct_array_size ty) (array_size elemty)
+ else direct_array_size ty
+ | TArray(_,None,_,_) -> Integer.zero
+ | _ -> assert false
let direct_element_type ty = match unrollType ty with
| TArray(eltyp,_,_,_) -> eltyp
@@ -417,18 +421,18 @@ let element_type ty =
| _ -> ty
in
match unrollType ty with
- | TArray(eltyp,_,_,_) -> elem_type eltyp
- | _ -> assert false
+ | TArray(eltyp,_,_,_) -> elem_type eltyp
+ | _ -> assert false
let direct_pointed_type ty =
match unrollType ty with
- | TPtr(elemty,_) -> elemty
- | _ -> assert false
+ | TPtr(elemty,_) -> elemty
+ | _ -> assert false
let pointed_type ty =
match unrollType (direct_pointed_type ty) with
- | TArray _ as arrty -> element_type arrty
- | ty -> ty
+ | TArray _ as arrty -> element_type arrty
+ | ty -> ty
(* ************************************************************************** *)
(** {2 Predefined} *)
@@ -460,7 +464,7 @@ let is_frama_c_builtin n =
is_cea_domain_function n ||
is_cea_dump_file_function n)
-let () = Cil.add_special_builtin_family is_frama_c_builtin
+let () = Cil_builtins.add_special_builtin_family is_frama_c_builtin
(*
Local Variables:
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 6d4ecc5dec010c913bd9890d7527ee471f25241c..22cef1f703033543f59da7d347470cd9e330fa71 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -62,56 +62,57 @@ val possible_value_of_integral_term: term -> Integer.t option
@since Oxygen-20120901 *)
val term_lvals_of_term: term -> term_lval list
- (** @return the list of all the term lvals of a given term.
- Purely syntactic function. *)
+(** @return the list of all the term lvals of a given term.
+ Purely syntactic function. *)
val precondition : funspec -> predicate
- (** Builds the precondition from [b_assumes] and [b_requires] clauses.
- @since Carbon-20101201 *)
+(** Builds the precondition from [b_assumes] and [b_requires] clauses.
+ @since Carbon-20101201 *)
val behavior_assumes : funbehavior -> predicate
- (** Builds the conjunction of the [b_assumes].
- @since Nitrogen-20111001 *)
-
+(** Builds the conjunction of the [b_assumes].
+ @since Nitrogen-20111001 *)
+
val behavior_precondition : funbehavior -> predicate
- (** Builds the precondition from [b_assumes] and [b_requires] clauses.
- @since Carbon-20101201 *)
+(** Builds the precondition from [b_assumes] and [b_requires] clauses.
+ @since Carbon-20101201 *)
val behavior_postcondition : funbehavior -> termination_kind -> predicate
- (** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
- @modify Boron-20100401 added termination kind as filtering argument. *)
+(** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
+ @modify Boron-20100401 added termination kind as filtering argument. *)
val disjoint_behaviors : funspec -> string list -> predicate
- (** Builds the [disjoint_behaviors] property for the behavior names.
- @since Nitrogen-20111001 *)
+(** Builds the [disjoint_behaviors] property for the behavior names.
+ @since Nitrogen-20111001 *)
val complete_behaviors : funspec -> string list -> predicate
- (** Builds the [disjoint_behaviors] property for the behavior names.
- @since Nitrogen-20111001 *)
+(** Builds the [disjoint_behaviors] property for the behavior names.
+ @since Nitrogen-20111001 *)
-val merge_assigns_from_complete_bhvs:
+val merge_assigns_from_complete_bhvs:
?warn:bool -> ?unguarded:bool -> funbehavior list -> string list list -> assigns
- (** @return the assigns of an unguarded behavior (when [unguarded]=true)
- or a set of complete behaviors.
- - the funbehaviors can come from either a statement contract or a function
- contract.
- - the list of sets of behavior names can come from the contract of the
+(** @return the assigns of an unguarded behavior (when [unguarded]=true)
+ or a set of complete behaviors.
+ - the funbehaviors can come from either a statement contract or a function
+ contract.
+ - the list of sets of behavior names can come from the contract of the
related function.
- Optional [warn] argument can be used to force emitting or cancelation of
- warnings.
- @since Oxygen-20120901 *)
+
+ Optional [warn] argument can be used to force emitting or cancelation of
+ warnings.
+ @since Oxygen-20120901 *)
val merge_assigns_from_spec: ?warn:bool -> funspec -> assigns
(** It is a shortcut for [merge_assigns_from_complete_bhvs
spec.spec_complete_behaviors spec.spec_behavior]. Optional [warn] argument
- can be used to force emitting or cancelation of warnings
+ can be used to force emitting or cancelation of warnings
@return the assigns of an unguarded behavior or a set of complete behaviors.
- @since Oxygen-20120901 *)
+ @since Oxygen-20120901 *)
val merge_assigns: ?warn:bool -> funbehavior list -> assigns
-(** Returns the assigns of an unguarded behavior.
+(** Returns the assigns of an unguarded behavior.
@modify Oxygen-20120901 Optional [warn] argument added which can be used to
- force emitting or cancelation of warnings. *)
+ force emitting or cancelation of warnings. *)
val variable_term: location -> logic_var -> term
val constant_term: location -> Integer.t -> term
@@ -153,21 +154,21 @@ val pointed_type: typ -> typ
(* ************************************************************************** *)
val is_function_type : varinfo -> bool
- (** Return [true] iff the type of the given varinfo is a function type. *)
+(** Return [true] iff the type of the given varinfo is a function type. *)
(** Operations on cil function. *)
module Function: sig
val formal_args: varinfo -> (string * typ * attributes) list
- (** Returns the list of the named formal arguments of a function.
- Never call on a variable of non functional type.*)
+ (** Returns the list of the named formal arguments of a function.
+ Never call on a variable of non functional type.*)
val is_formal: varinfo -> fundec -> bool
val is_local: varinfo -> fundec -> bool
val is_formal_or_local: varinfo -> fundec -> bool
val is_formal_of_prototype:
varinfo (* to check *) -> varinfo (* of the prototype *) -> bool
- (** [is_formal_of_prototype v f] returns [true] iff [f] is a prototype and
- [v] is one of its formal parameters. *)
+ (** [is_formal_of_prototype v f] returns [true] iff [f] is a prototype and
+ [v] is one of its formal parameters. *)
val is_definition: cil_function -> bool
val get_vi: cil_function -> varinfo
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index f3f919e645da4b181c4c8d8b78b15b0ff7376e75..fd327796b0b2d13459f7fabe0f203da3d65ef50a 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -453,7 +453,6 @@ let typeHasAttributeMemoryBlock a (ty:typ): bool =
try visit ty; false
with Exit -> true
-let typeAddVolatile typ = typeAddAttributes [Attr ("volatile", [])] typ
let typeAddGhost typ =
if not (typeHasAttribute "ghost" typ) then
typeAddAttributes [Attr ("ghost", [])] typ
@@ -4862,389 +4861,6 @@ let interpret_character_constant char_list =
end
let invalidStmt = mkStmt (Instr (Skip Location.unknown))
-module Frama_c_builtins =
- State_builder.Hashtbl
- (Datatype.String.Hashtbl)
- (Cil_datatype.Varinfo)
- (struct
- let name = "Cil.Frama_c_Builtins"
- let dependencies = []
- let size = 3
- end)
-
-let () = dependency_on_ast Frama_c_builtins.self
-
-let is_builtin v = hasAttribute "FC_BUILTIN" v.vattr
-
-let is_unused_builtin v = is_builtin v && not v.vreferenced
-
-
-(* [VP] Should we projectify this ?*)
-let special_builtins_table = ref Datatype.String.Set.empty
-let special_builtins = Queue.create ()
-
-let is_special_builtin s =
- Queue.fold (fun res f -> res || f s) false special_builtins
-
-let add_special_builtin_family f = Queue.add f special_builtins
-
-let add_special_builtin s =
- special_builtins_table := Datatype.String.Set.add s !special_builtins_table
-
-let () = add_special_builtin_family
- (fun s -> Datatype.String.Set.mem s !special_builtins_table)
-
-let () = List.iter add_special_builtin
- [ "__builtin_stdarg_start"; "__builtin_va_arg";
- "__builtin_va_start"; "__builtin_expect"; "__builtin_next_arg"; ]
-
-module Builtin_functions =
- State_builder.Hashtbl
- (Datatype.String.Hashtbl)
- (Datatype.Triple(Typ)(Datatype.List(Typ))(Datatype.Bool))
- (struct
- let name = "Builtin_functions"
- let dependencies = [ TheMachine.self ]
- let size = 49
- end)
-
-let add_builtin ?(prefix="__builtin_") s t l b =
- Builtin_functions.add (prefix ^ s) (t, l, b)
-
-let () = registerAttribute "FC_BUILTIN" (AttrName true)
-
-(* Initialize the builtin functions after the machine has been initialized. *)
-let initGccBuiltins () : unit =
- let sizeType = theMachine.upointType in
- let add = add_builtin in
- add "__fprintf_chk"
- intType
- (* first argument is really FILE*, not void*, but we don't want to build in
- the definition for FILE *)
- [ voidPtrType; intType; charConstPtrType ]
- true;
- add "__memcpy_chk"
- voidPtrType
- [ voidPtrType; voidConstPtrType; sizeType; sizeType ]
- false;
- add "__memmove_chk"
- voidPtrType [ voidPtrType; voidConstPtrType; sizeType; sizeType ] false;
- add "__mempcpy_chk"
- voidPtrType [ voidPtrType; voidConstPtrType; sizeType; sizeType ] false;
- add "__memset_chk"
- voidPtrType [ voidPtrType; intType; sizeType; sizeType ] false;
- add "__printf_chk" intType [ intType; charConstPtrType ] true;
- add "__snprintf_chk"
- intType [ charPtrType; sizeType; intType; sizeType; charConstPtrType ]
- true;
- add "__sprintf_chk"
- intType [ charPtrType; intType; sizeType; charConstPtrType ] true;
- add "__stpcpy_chk"
- charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
- add "__strcat_chk"
- charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
- add "__strcpy_chk"
- charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
- add "__strncat_chk"
- charPtrType [ charPtrType; charConstPtrType; sizeType; sizeType ] false;
- add "__strncpy_chk"
- charPtrType [ charPtrType; charConstPtrType; sizeType; sizeType ] false;
- add "__vfprintf_chk"
- intType
- (* first argument is really FILE*, not void*, but we don't want to build in
- the definition for FILE *)
- [ voidPtrType; intType; charConstPtrType; TBuiltin_va_list [] ]
- false;
- add "__vprintf_chk"
- intType [ intType; charConstPtrType; TBuiltin_va_list [] ] false;
- add "__vsnprintf_chk"
- intType
- [ charPtrType; sizeType; intType; sizeType; charConstPtrType;
- TBuiltin_va_list [] ]
- false;
- add "__vsprintf_chk"
- intType
- [ charPtrType; intType; sizeType; charConstPtrType; TBuiltin_va_list [] ]
- false;
-
- add "alloca" voidPtrType [ sizeType ] false;
-
- add "acos" doubleType [ doubleType ] false;
- add "acosf" floatType [ floatType ] false;
- add "acosl" longDoubleType [ longDoubleType ] false;
-
- add "asin" doubleType [ doubleType ] false;
- add "asinf" floatType [ floatType ] false;
- add "asinl" longDoubleType [ longDoubleType ] false;
-
- add "atan" doubleType [ doubleType ] false;
- add "atanf" floatType [ floatType ] false;
- add "atanl" longDoubleType [ longDoubleType ] false;
-
- add "atan2" doubleType [ doubleType; doubleType ] false;
- add "atan2f" floatType [ floatType; floatType ] false;
- add "atan2l" longDoubleType [ longDoubleType;
- longDoubleType ] false;
-
- let uint16t = uint16_t () in
- add "bswap16" uint16t [uint16t] false;
-
- let uint32t = uint32_t () in
- add "bswap32" uint32t [uint32t] false;
-
- let uint64t = uint64_t () in
- add "bswap64" uint64t [uint64t] false;
-
- add "ceil" doubleType [ doubleType ] false;
- add "ceilf" floatType [ floatType ] false;
- add "ceill" longDoubleType [ longDoubleType ] false;
-
- add "cos" doubleType [ doubleType ] false;
- add "cosf" floatType [ floatType ] false;
- add "cosl" longDoubleType [ longDoubleType ] false;
-
- add "cosh" doubleType [ doubleType ] false;
- add "coshf" floatType [ floatType ] false;
- add "coshl" longDoubleType [ longDoubleType ] false;
-
- add "constant_p" intType [ intType ] false;
-
- add "exp" doubleType [ doubleType ] false;
- add "expf" floatType [ floatType ] false;
- add "expl" longDoubleType [ longDoubleType ] false;
-
- add "expect" longType [ longType; longType ] false;
-
- add "fabs" doubleType [ doubleType ] false;
- add "fabsf" floatType [ floatType ] false;
- add "fabsl" longDoubleType [ longDoubleType ] false;
-
- add "ffs" intType [ uintType ] false;
- add "ffsl" intType [ ulongType ] false;
- add "ffsll" intType [ ulongLongType ] false;
- add "frame_address" voidPtrType [ uintType ] false;
-
- add "floor" doubleType [ doubleType ] false;
- add "floorf" floatType [ floatType ] false;
- add "floorl" longDoubleType [ longDoubleType ] false;
-
- add "huge_val" doubleType [] false;
- add "huge_valf" floatType [] false;
- add "huge_vall" longDoubleType [] false;
- add "ia32_lfence" voidType [] false;
- add "ia32_mfence" voidType [] false;
- add "ia32_sfence" voidType [] false;
-
- add "inf" doubleType [] false;
- add "inff" floatType [] false;
- add "infl" longDoubleType [] false;
- add "memcpy" voidPtrType [ voidPtrType; voidConstPtrType; sizeType ] false;
- add "mempcpy" voidPtrType [ voidPtrType; voidConstPtrType; sizeType ] false;
- add "memset" voidPtrType [ voidPtrType; intType; intType ] false;
-
- add "fmod" doubleType [ doubleType ] false;
- add "fmodf" floatType [ floatType ] false;
- add "fmodl" longDoubleType [ longDoubleType ] false;
-
- add "frexp" doubleType [ doubleType; intPtrType ] false;
- add "frexpf" floatType [ floatType; intPtrType ] false;
- add "frexpl" longDoubleType [ longDoubleType; intPtrType ] false;
-
- add "ldexp" doubleType [ doubleType; intType ] false;
- add "ldexpf" floatType [ floatType; intType ] false;
- add "ldexpl" longDoubleType [ longDoubleType; intType ] false;
-
- add "log" doubleType [ doubleType ] false;
- add "logf" floatType [ floatType ] false;
- add "logl" longDoubleType [ longDoubleType ] false;
-
- add "log10" doubleType [ doubleType ] false;
- add "log10f" floatType [ floatType ] false;
- add "log10l" longDoubleType [ longDoubleType ] false;
-
- add "modff" floatType [ floatType; TPtr(floatType,[]) ] false;
- add "modfl"
- longDoubleType [ longDoubleType; TPtr(longDoubleType, []) ] false;
-
- add "nan" doubleType [ charConstPtrType ] false;
- add "nanf" floatType [ charConstPtrType ] false;
- add "nanl" longDoubleType [ charConstPtrType ] false;
- add "nans" doubleType [ charConstPtrType ] false;
- add "nansf" floatType [ charConstPtrType ] false;
- add "nansl" longDoubleType [ charConstPtrType ] false;
- add "object_size" sizeType [ voidPtrType; intType ] false;
-
- add "parity" intType [ uintType ] false;
- add "parityl" intType [ ulongType ] false;
- add "parityll" intType [ ulongLongType ] false;
-
- add "powi" doubleType [ doubleType; intType ] false;
- add "powif" floatType [ floatType; intType ] false;
- add "powil" longDoubleType [ longDoubleType; intType ] false;
- add "prefetch" voidType [ voidConstPtrType ] true;
- add "return" voidType [ voidConstPtrType ] false;
- add "return_address" voidPtrType [ uintType ] false;
-
- add "sin" doubleType [ doubleType ] false;
- add "sinf" floatType [ floatType ] false;
- add "sinl" longDoubleType [ longDoubleType ] false;
-
- add "sinh" doubleType [ doubleType ] false;
- add "sinhf" floatType [ floatType ] false;
- add "sinhl" longDoubleType [ longDoubleType ] false;
-
- add "sqrt" doubleType [ doubleType ] false;
- add "sqrtf" floatType [ floatType ] false;
- add "sqrtl" longDoubleType [ longDoubleType ] false;
-
- add "stpcpy" charPtrType [ charPtrType; charConstPtrType ] false;
- add "strchr" charPtrType [ charPtrType; intType ] false;
- add "strcmp" intType [ charConstPtrType; charConstPtrType ] false;
- add "strcpy" charPtrType [ charPtrType; charConstPtrType ] false;
- add "strcspn" sizeType [ charConstPtrType; charConstPtrType ] false;
- add "strncat" charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
- add "strncmp" intType [ charConstPtrType; charConstPtrType; sizeType ] false;
- add "strncpy" charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
- add "strspn" sizeType [ charConstPtrType; charConstPtrType ] false;
- add "strpbrk" charPtrType [ charConstPtrType; charConstPtrType ] false;
- (* When we parse builtin_types_compatible_p, we change its interface *)
- add "types_compatible_p"
- intType
- [ theMachine.typeOfSizeOf;(* Sizeof the type *)
- theMachine.typeOfSizeOf (* Sizeof the type *) ]
- false;
- add "tan" doubleType [ doubleType ] false;
- add "tanf" floatType [ floatType ] false;
- add "tanl" longDoubleType [ longDoubleType ] false;
-
- add "tanh" doubleType [ doubleType ] false;
- add "tanhf" floatType [ floatType ] false;
- add "tanhl" longDoubleType [ longDoubleType ] false;
-
- add "unreachable" voidType [ ] false;
-
- let int8_t = Some scharType in
- let int16_t = try Some (int16_t ()) with Not_found -> None in
- let int32_t = try Some (int32_t ()) with Not_found -> None in
- let int64_t = try Some (int64_t ()) with Not_found -> None in
- let uint8_t = Some ucharType in
- let uint16_t = try Some (uint16_t ()) with Not_found -> None in
- let uint32_t = try Some (uint32_t ()) with Not_found -> None in
- let uint64_t = try Some (uint64_t ()) with Not_found -> None in
-
- (* Binary monomorphic versions of atomic builtins *)
- let atomic_instances =
- [int8_t, "_int8_t";
- int16_t,"_int16_t";
- int32_t,"_int32_t";
- int64_t,"_int64_t";
- uint8_t, "_uint8_t";
- uint16_t,"_uint16_t";
- uint32_t,"_uint32_t";
- uint64_t,"_uint64_t"]
- in
- let add_sync (typ,name) f =
- match typ with
- | Some typ ->
- add ~prefix:"__sync_" (f^name) typ [ TPtr(typeAddVolatile typ,[]); typ] true
- | None -> ()
- in
- let add_sync f =
- List.iter (fun typ -> add_sync typ f) atomic_instances
- in
- add_sync "fetch_and_add";
- add_sync "fetch_and_sub";
- add_sync "fetch_and_or";
- add_sync "fetch_and_and";
- add_sync "fetch_and_xor";
- add_sync "fetch_and_nand";
- add_sync "add_and_fetch";
- add_sync "sub_and_fetch";
- add_sync "or_and_fetch";
- add_sync "and_and_fetch";
- add_sync "xor_and_fetch";
- add_sync "nand_and_fetch";
- add_sync "lock_test_and_set";
- List.iter (fun (typ,n) ->
- match typ with
- | Some typ ->
- add ~prefix:"" ("__sync_bool_compare_and_swap"^n)
- intType
- [ TPtr(typeAddVolatile typ,[]); typ ; typ]
- true
- | None -> ())
- atomic_instances;
- List.iter (fun (typ,n) ->
- match typ with
- | Some typ ->
- add ~prefix:"" ("__sync_val_compare_and_swap"^n)
- typ
- [ TPtr(typeAddVolatile typ,[]); typ ; typ]
- true
- | None -> ())
- atomic_instances;
- List.iter (fun (typ,n) ->
- match typ with
- | Some typ ->
- add ~prefix:"" ("__sync_lock_release"^n)
- voidType
- [ TPtr(typeAddVolatile typ,[]) ]
- true;
- | None -> ())
- atomic_instances;
- add ~prefix:"" "__sync_synchronize" voidType [] true
-;;
-
-(* Builtins related to va_list. Added to all non-msvc machdeps, because
- Cabs2cil supposes they exist. *)
-let initVABuiltins () =
- let hasbva = theMachine.theMachine.has__builtin_va_list in
- let add = add_builtin in
- add "next_arg"
- (* When we parse builtin_next_arg we drop the second argument *)
- (if hasbva then TBuiltin_va_list [] else voidPtrType) [] false;
- if hasbva then begin
- add "va_end" voidType [ TBuiltin_va_list [] ] false;
- add "varargs_start" voidType [ TBuiltin_va_list [] ] false;
- (* When we parse builtin_{va,stdarg}_start, we drop the second argument *)
- add "va_start" voidType [ TBuiltin_va_list [] ] false;
- add "stdarg_start" voidType [ TBuiltin_va_list [] ] false;
- (* When we parse builtin_va_arg we change its interface *)
- add "va_arg"
- voidType
- [ TBuiltin_va_list [];
- theMachine.typeOfSizeOf;(* Sizeof the type *)
- voidPtrType (* Ptr to res *) ]
- false;
- add "va_copy" voidType [ TBuiltin_va_list []; TBuiltin_va_list [] ] false;
- end
-
-let initMsvcBuiltins () : unit =
- (** Take a number of wide string literals *)
- Builtin_functions.add "__annotation" (voidType, [ ], true)
-
-let init_common_builtins () =
- add_builtin
- "offsetof"
- theMachine.typeOfSizeOf
- [ theMachine.typeOfSizeOf ]
- false
-
-let init_builtins () =
- if not (TheMachine.is_computed ()) then
- Kernel.fatal ~current:true "You must call initCIL before init_builtins" ;
- if Builtin_functions.length () <> 0 then
- Kernel.fatal ~current:true "Cil builtins already initialized." ;
- init_common_builtins ();
- if msvcMode () then
- initMsvcBuiltins ()
- else begin
- initVABuiltins ();
- if gccMode () then initGccBuiltins ();
- end
-
-(** This is used as the location of the prototypes of builtin functions. *)
-let builtinLoc: location = Location.unknown
let range_loc loc1 loc2 = fst loc1, snd loc2
@@ -6611,6 +6227,8 @@ let is_case_label l = match l with
| Case _ | Default _ -> true
| _ -> false
+let init_builtins_ref : (unit -> unit) ref = Extlib.mk_fun "init_builtins_ref"
+
let initCIL ~initLogicBuiltins machdep =
if not (TheMachine.is_computed ()) then begin
(* Set the machine *)
@@ -6672,7 +6290,7 @@ let initCIL ~initLogicBuiltins machdep =
(* projectify theMachine *)
copyMachine theMachine !theMachineProject;
- init_builtins ();
+ !init_builtins_ref ();
Logic_env.Builtins.extend initLogicBuiltins;
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 60d2376a79df9ff31ac26fa6f68d96753423999d..4b74ee936bb7666e86ea6793117cbd0a11563fe3 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -51,46 +51,6 @@
open Cil_types
open Cil_datatype
-(* ************************************************************************* *)
-(** {2 Builtins management} *)
-(* ************************************************************************* *)
-
-(** This module associates the name of a built-in function that might be used
- during elaboration with the corresponding varinfo. This is done when
- parsing ${FRAMAC_SHARE}/libc/__fc_builtins.h, which is always performed
- before processing the actual list of files provided on the command line (see
- {!File.init_from_c_files}). Actual list of such built-ins is managed in
- {!Cabs2cil}. *)
-module Frama_c_builtins:
- State_builder.Hashtbl with type key = string and type data = Cil_types.varinfo
-
-val is_builtin: Cil_types.varinfo -> bool
-(** @return true if the given variable refers to a Frama-C builtin.
- @since Fluorine-20130401 *)
-
-val is_unused_builtin: Cil_types.varinfo -> bool
-(** @return true if the given variable refers to a Frama-C builtin that
- is not used in the current program. Plugins may (and in fact should)
- hide this builtin from their outputs *)
-
-val is_special_builtin: string -> bool
-(** @return [true] if the given name refers to a special built-in function.
- A special built-in function can have any number of arguments. It is up to
- the plug-ins to know what to do with it.
- @since Carbon-20101201 *)
-
-(** register a new special built-in function *)
-val add_special_builtin: string -> unit
-
-(** register a new family of special built-in functions.
- @since Carbon-20101201
-*)
-val add_special_builtin_family: (string -> bool) -> unit
-
-(** initialize the C built-ins. Should be called once per project, after the
- machine has been set. *)
-val init_builtins: unit -> unit
-
(** Call this function to perform some initialization, and only after you have
set [Cil.msvcMode]. [initLogicBuiltins] is the function to call to init
logic builtins. The [Machdeps] argument is a description of the hardware
@@ -266,20 +226,6 @@ val pushGlobal: global -> types: global list ref
(** An empty statement. Used in pretty printing *)
val invalidStmt: stmt
-(** A list of the built-in functions for the current compiler (GCC or
- * MSVC, depending on [!msvcMode]). Maps the name to the
- * result and argument types, and whether it is vararg.
- * Initialized by {!Cil.initCIL}
- *
- * This map replaces [gccBuiltins] and [msvcBuiltins] in previous
- * versions of CIL.*)
-module Builtin_functions :
- State_builder.Hashtbl with type key = string
- and type data = typ * typ list * bool
-
-(** This is used as the location of the prototypes of builtin functions. *)
-val builtinLoc: location
-
(** Returns a location that ranges over the two locations in arguments. *)
val range_loc: location -> location -> location
@@ -351,10 +297,34 @@ val ulongType: typ
(** unsigned long long *)
val ulongLongType: typ
+(** Any signed integer type of size 16 bits.
+ It is equivalent to the ISO C int16_t type but without using the
+ corresponding header.
+ Must only be called if such type exists in the current architecture.
+ @since Frama-C+dev
+*)
+val int16_t: unit -> typ
+
+(** Any signed integer type of size 32 bits.
+ It is equivalent to the ISO C int32_t type but without using the
+ corresponding header.
+ Must only be called if such type exists in the current architecture.
+ @since Frama-C+dev
+*)
+val int32_t: unit -> typ
+
+(** Any signed integer type of size 64 bits.
+ It is equivalent to the ISO C int64_t type but without using the
+ corresponding header.
+ Must only be called if such type exists in the current architecture.
+ @since Frama-C+dev
+*)
+val int64_t: unit -> typ
+
(** Any unsigned integer type of size 16 bits.
It is equivalent to the ISO C uint16_t type but without using the
corresponding header.
- Shall not be called if not such type exists in the current architecture.
+ Must only be called if such type exists in the current architecture.
@since Nitrogen-20111001
*)
val uint16_t: unit -> typ
@@ -362,7 +332,7 @@ val uint16_t: unit -> typ
(** Any unsigned integer type of size 32 bits.
It is equivalent to the ISO C uint32_t type but without using the
corresponding header.
- Shall not be called if not such type exists in the current architecture.
+ Must only be called if such type exists in the current architecture.
@since Nitrogen-20111001
*)
val uint32_t: unit -> typ
@@ -370,7 +340,7 @@ val uint32_t: unit -> typ
(** Any unsigned integer type of size 64 bits.
It is equivalent to the ISO C uint64_t type but without using the
corresponding header.
- Shall not be called if no such type exists in the current architecture.
+ Must only be called if such type exists in the current architecture.
@since Nitrogen-20111001
*)
val uint64_t: unit -> typ
@@ -2354,6 +2324,12 @@ val set_deprecated_extension_handler:
(cilVisitor -> acsl_extension_kind -> acsl_extension_kind visitAction) ->
unit) -> unit
+(* ***********************************************************************)
+(** {2 Forward references} *)
+(* ***********************************************************************)
+
+val init_builtins_ref: (unit -> unit) ref
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
new file mode 100644
index 0000000000000000000000000000000000000000..94d8a3a62efb9e5a14bcda569a26f697ecf8ad9d
--- /dev/null
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -0,0 +1,705 @@
+(****************************************************************************)
+(* *)
+(* Copyright (C) 2001-2003 *)
+(* George C. Necula <necula@cs.berkeley.edu> *)
+(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
+(* Wes Weimer <weimer@cs.berkeley.edu> *)
+(* Ben Liblit <liblit@cs.berkeley.edu> *)
+(* All rights reserved. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in the *)
+(* documentation and/or other materials provided with the distribution. *)
+(* *)
+(* 3. The names of the contributors may not be used to endorse or *)
+(* promote products derived from this software without specific prior *)
+(* written permission. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
+(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
+(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
+(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
+(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
+(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
+(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
+(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
+(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
+(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
+(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
+(* POSSIBILITY OF SUCH DAMAGE. *)
+(* *)
+(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
+(* énergies alternatives) *)
+(* and INRIA (Institut National de Recherche en Informatique *)
+(* et Automatique). *)
+(****************************************************************************)
+
+open Cil_datatype
+open Cil_types
+
+let typeAddVolatile typ = Cil.typeAddAttributes [Attr ("volatile", [])] typ
+
+module Frama_c_builtins =
+ State_builder.Hashtbl
+ (Datatype.String.Hashtbl)
+ (Cil_datatype.Varinfo)
+ (struct
+ let name = "Cil.Frama_c_Builtins"
+ let dependencies = []
+ let size = 3
+ end)
+
+let () = Cil.dependency_on_ast Frama_c_builtins.self
+
+let is_builtin v = Cil.hasAttribute "FC_BUILTIN" v.vattr
+
+let is_unused_builtin v = is_builtin v && not v.vreferenced
+
+
+(* [VP] Should we projectify this ?*)
+let special_builtins_table = ref Datatype.String.Set.empty
+let special_builtins = Queue.create ()
+
+let is_special_builtin s =
+ Queue.fold (fun res f -> res || f s) false special_builtins
+
+let add_special_builtin_family f = Queue.add f special_builtins
+
+let add_special_builtin s =
+ special_builtins_table := Datatype.String.Set.add s !special_builtins_table
+
+let () = add_special_builtin_family
+ (fun s -> Datatype.String.Set.mem s !special_builtins_table)
+
+let () = List.iter add_special_builtin
+ [ "__builtin_stdarg_start"; "__builtin_va_arg";
+ "__builtin_va_start"; "__builtin_expect"; "__builtin_next_arg"; ]
+
+module Builtin_functions =
+ State_builder.Hashtbl
+ (Datatype.String.Hashtbl)
+ (Datatype.Triple(Typ)(Datatype.List(Typ))(Datatype.Bool))
+ (struct
+ let name = "Builtin_functions"
+ let dependencies = [ Cil.selfMachine ]
+ let size = 49
+ end)
+
+(* [add_builtin ?prefix s t l b] adds the function [prefix ^ s] to the list of
+ built-ins. [t] is the return type and [l] is the list of parameter types.
+ [b] is true if the built-in is variadic, false otherwise. *)
+let add_builtin ?(prefix="__builtin_") s t l b =
+ Builtin_functions.add (prefix ^ s) (t, l, b)
+
+let () = Cil.registerAttribute "FC_BUILTIN" (AttrName true)
+
+let intType = Cil.intType
+let voidPtrType = Cil.voidPtrType
+let charConstPtrType = Cil.charConstPtrType
+let voidConstPtrType = Cil.voidConstPtrType
+let charPtrType = Cil.charPtrType
+let voidType = Cil.voidType
+let floatType = Cil.floatType
+let doubleType = Cil.doubleType
+let longDoubleType = Cil.longDoubleType
+let longType = Cil.longType
+let longLongType = Cil.longLongType
+let uintType = Cil.uintType
+let ulongType = Cil.ulongType
+let ulongLongType = Cil.ulongLongType
+let intPtrType = Cil.intPtrType
+
+(* Initialize the builtin functions after the machine has been initialized. *)
+let initGccBuiltins () : unit =
+ (* Complex types are unsupported so the following built-ins can't be added :
+ - cabs, cabsf, cabsh
+ - cacos, cacosf, cacosl, cacosh, cacoshf, cacoshl
+ - carg, cargf, cargl
+ - casin, casinf, casinl, casinh, casinhf, casinhl
+ - catan, catanf, catanl, catanh, catanhf, catanhl
+ - ccos, ccosf, ccosl, ccosh, ccoshf, ccoshl
+ - cexp, cexpf, cexpl
+ - cimag, cimagf, cimagl
+ - clog, clogf, clogl
+ - conj, conjf, conjl
+ - cpow, cpowf, cpowl
+ - cproj, cprojf, cprojl
+ - creal, crealf, creall
+ - csin, csinf, csinl, csinh, csinhf, csinhl
+ - csqrt, csqrtf, csqrtl
+ - ctan, ctanf, ctanl, ctanh, ctanhf, ctanhl
+ *)
+
+ (* [wint_t] isn't specified in [theMachine] so the following built-ins that
+ use this type can't be added :
+ - iswalnum
+ - iswalpha
+ - iswblank
+ - iswcntrl
+ - iswdigit
+ - iswgraph
+ - iswlower
+ - iswprint
+ - iswpunct
+ - iswspace
+ - iswupper
+ - iswxdigit
+ - towlower
+ - towupper
+ *)
+
+ let sizeType = Cil.theMachine.upointType in
+ let add = add_builtin in
+
+ add "__fprintf_chk"
+ intType
+ (* first argument is really FILE*, not void*, but we don't want to build in
+ the definition for FILE *)
+ [ voidPtrType; intType; charConstPtrType ]
+ true;
+ add "__memcpy_chk"
+ voidPtrType
+ [ voidPtrType; voidConstPtrType; sizeType; sizeType ]
+ false;
+ add "__memmove_chk"
+ voidPtrType [ voidPtrType; voidConstPtrType; sizeType; sizeType ] false;
+ add "__mempcpy_chk"
+ voidPtrType [ voidPtrType; voidConstPtrType; sizeType; sizeType ] false;
+ add "__memset_chk"
+ voidPtrType [ voidPtrType; intType; sizeType; sizeType ] false;
+ add "__printf_chk" intType [ intType; charConstPtrType ] true;
+ add "__snprintf_chk"
+ intType [ charPtrType; sizeType; intType; sizeType; charConstPtrType ]
+ true;
+ add "__sprintf_chk"
+ intType [ charPtrType; intType; sizeType; charConstPtrType ] true;
+ add "__stpcpy_chk"
+ charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
+ add "__strcat_chk"
+ charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
+ add "__strcpy_chk"
+ charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
+ add "__strncat_chk"
+ charPtrType [ charPtrType; charConstPtrType; sizeType; sizeType ] false;
+ add "__strncpy_chk"
+ charPtrType [ charPtrType; charConstPtrType; sizeType; sizeType ] false;
+ add "__vfprintf_chk"
+ intType
+ (* first argument is really FILE*, not void*, but we don't want to build in
+ the definition for FILE *)
+ [ voidPtrType; intType; charConstPtrType; TBuiltin_va_list [] ]
+ false;
+ add "__vprintf_chk"
+ intType [ intType; charConstPtrType; TBuiltin_va_list [] ] false;
+ add "__vsnprintf_chk"
+ intType
+ [ charPtrType; sizeType; intType; sizeType; charConstPtrType;
+ TBuiltin_va_list [] ]
+ false;
+ add "__vsprintf_chk"
+ intType
+ [ charPtrType; intType; sizeType; charConstPtrType; TBuiltin_va_list [] ]
+ false;
+
+ add "_Exit" voidType [ intType ] false;
+ add "exit" voidType [ intType ] false;
+
+ add "alloca" voidPtrType [ sizeType ] false;
+
+ add "malloc" voidPtrType [ sizeType ] false;
+ add "calloc" voidPtrType [ sizeType; sizeType ] false;
+ add "realloc" voidPtrType [ voidPtrType; sizeType ] false;
+ add "free" voidType [ voidPtrType ] false;
+
+ add "abs" intType [ intType ] false;
+ add "labs" longType [ longType ] false;
+ add "llabs" longLongType [ longLongType] false;
+ (* Can't add imaxabs because it takes intmax_t as parameter *)
+
+ add "acos" doubleType [ doubleType ] false;
+ add "acosf" floatType [ floatType ] false;
+ add "acosl" longDoubleType [ longDoubleType ] false;
+ add "acosh" doubleType [ doubleType ] false;
+ add "acoshf" floatType [ floatType ] false;
+ add "acoshl" longDoubleType [ longDoubleType ] false;
+
+ add "asin" doubleType [ doubleType ] false;
+ add "asinf" floatType [ floatType ] false;
+ add "asinl" longDoubleType [ longDoubleType ] false;
+ add "asinh" doubleType [ doubleType ] false;
+ add "asinhf" floatType [ floatType ] false;
+ add "asinhl" longDoubleType [ longDoubleType ] false;
+
+ add "atan" doubleType [ doubleType ] false;
+ add "atanf" floatType [ floatType ] false;
+ add "atanl" longDoubleType [ longDoubleType ] false;
+ add "atanh" doubleType [ doubleType ] false;
+ add "atanhf" floatType [ floatType ] false;
+ add "atanhl" longDoubleType [ longDoubleType ] false;
+
+ add "atan2" doubleType [ doubleType; doubleType ] false;
+ add "atan2f" floatType [ floatType; floatType ] false;
+ add "atan2l" longDoubleType [ longDoubleType;
+ longDoubleType ] false;
+
+ let uint16t = Cil.uint16_t () in
+ add "bswap16" uint16t [uint16t] false;
+
+ let uint32t = Cil.uint32_t () in
+ add "bswap32" uint32t [uint32t] false;
+
+ let uint64t = Cil.uint64_t () in
+ add "bswap64" uint64t [uint64t] false;
+
+ add "cbrt" doubleType [ doubleType ] false;
+ add "cbrtf" floatType [ floatType ] false;
+ add "cbrtl" longDoubleType [ longDoubleType ] false;
+
+ add "ceil" doubleType [ doubleType ] false;
+ add "ceilf" floatType [ floatType ] false;
+ add "ceill" longDoubleType [ longDoubleType ] false;
+
+ add "cos" doubleType [ doubleType ] false;
+ add "cosf" floatType [ floatType ] false;
+ add "cosl" longDoubleType [ longDoubleType ] false;
+
+ add "cosh" doubleType [ doubleType ] false;
+ add "coshf" floatType [ floatType ] false;
+ add "coshl" longDoubleType [ longDoubleType ] false;
+
+ add "constant_p" intType [ intType ] false;
+
+ add "copysign" doubleType [ doubleType; doubleType ] false;
+ add "copysignf" floatType [ floatType; floatType ] false;
+ add "copysignl" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "erfc" doubleType [ doubleType ] false;
+ add "erfcf" floatType [ floatType ] false;
+ add "erfcl" longDoubleType [ longDoubleType ] false;
+
+ add "erf" doubleType [ doubleType ] false;
+ add "erff" floatType [ floatType ] false;
+ add "erfl" longDoubleType [ longDoubleType ] false;
+
+ add "exp" doubleType [ doubleType ] false;
+ add "expf" floatType [ floatType ] false;
+ add "expl" longDoubleType [ longDoubleType ] false;
+
+ add "exp2" doubleType [ doubleType ] false;
+ add "exp2f" floatType [ floatType ] false;
+ add "exp2l" longDoubleType [ longDoubleType ] false;
+
+ add "expm1" doubleType [ doubleType ] false;
+ add "expm1f" floatType [ floatType ] false;
+ add "expm1l" longDoubleType [ longDoubleType ] false;
+
+ add "expect" longType [ longType; longType ] false;
+
+ add "fabs" doubleType [ doubleType ] false;
+ add "fabsf" floatType [ floatType ] false;
+ add "fabsl" longDoubleType [ longDoubleType ] false;
+
+ add "fdim" doubleType [ doubleType; doubleType ] false;
+ add "fdimf" floatType [ floatType; floatType ] false;
+ add "fdiml" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "ffs" intType [ uintType ] false;
+ add "ffsl" intType [ ulongType ] false;
+ add "ffsll" intType [ ulongLongType ] false;
+ add "frame_address" voidPtrType [ uintType ] false;
+
+ add "floor" doubleType [ doubleType ] false;
+ add "floorf" floatType [ floatType ] false;
+ add "floorl" longDoubleType [ longDoubleType ] false;
+
+ add "fma" doubleType [ doubleType; doubleType; doubleType ] false;
+ add "fmaf" floatType [ floatType; floatType; floatType ] false;
+ add "fmal"
+ longDoubleType [ longDoubleType; longDoubleType; longDoubleType ] false;
+
+ add "fmax" doubleType [ doubleType; doubleType ] false;
+ add "fmaxf" floatType [ floatType; floatType ] false;
+ add "fmaxl" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "fmin" doubleType [ doubleType; doubleType ] false;
+ add "fminf" floatType [ floatType; floatType ] false;
+ add "fminl" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "huge_val" doubleType [] false;
+ add "huge_valf" floatType [] false;
+ add "huge_vall" longDoubleType [] false;
+
+ add "hypot" doubleType [ doubleType; doubleType ] false;
+ add "hypotf" floatType [ floatType; floatType ] false;
+ add "hypotl" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "ia32_lfence" voidType [] false;
+ add "ia32_mfence" voidType [] false;
+ add "ia32_sfence" voidType [] false;
+
+ add "ilogb" doubleType [ doubleType ] false;
+ add "ilogbf" floatType [ floatType ] false;
+ add "ilogbl" longDoubleType [ longDoubleType ] false;
+
+ add "inf" doubleType [] false;
+ add "inff" floatType [] false;
+ add "infl" longDoubleType [] false;
+
+ add "isblank" intType [ intType ] false;
+ add "isalnum" intType [ intType ] false;
+ add "isalpha" intType [ intType ] false;
+ add "iscntrl" intType [ intType ] false;
+ add "isdigit" intType [ intType ] false;
+ add "isgraph" intType [ intType ] false;
+ add "islower" intType [ intType ] false;
+ add "isprint" intType [ intType ] false;
+ add "ispunct" intType [ intType ] false;
+ add "isspace" intType [ intType ] false;
+ add "isupper" intType [ intType ] false;
+ add "isxdigit" intType [ intType ] false;
+
+ add "fmod" doubleType [ doubleType ] false;
+ add "fmodf" floatType [ floatType ] false;
+ add "fmodl" longDoubleType [ longDoubleType ] false;
+
+ add "frexp" doubleType [ doubleType; intPtrType ] false;
+ add "frexpf" floatType [ floatType; intPtrType ] false;
+ add "frexpl" longDoubleType [ longDoubleType; intPtrType ] false;
+
+ add "ldexp" doubleType [ doubleType; intType ] false;
+ add "ldexpf" floatType [ floatType; intType ] false;
+ add "ldexpl" longDoubleType [ longDoubleType; intType ] false;
+
+ add "lgamma" doubleType [ doubleType ] false;
+ add "lgammaf" floatType [ floatType ] false;
+ add "lgammal" longDoubleType [ longDoubleType ] false;
+
+ add "llrint" longLongType [ doubleType ] false;
+ add "llrintf" longLongType [ floatType ] false;
+ add "llrintl" longLongType [ longDoubleType ] false;
+
+ add "llround" longLongType [ doubleType ] false;
+ add "llroundf" longLongType [ floatType ] false;
+ add "llroundl" longLongType [ longDoubleType ] false;
+
+ add "log" doubleType [ doubleType ] false;
+ add "logf" floatType [ floatType ] false;
+ add "logl" longDoubleType [ longDoubleType ] false;
+
+ add "log10" doubleType [ doubleType ] false;
+ add "log10f" floatType [ floatType ] false;
+ add "log10l" longDoubleType [ longDoubleType ] false;
+
+ add "log1p" doubleType [ doubleType ] false;
+ add "log1pf" floatType [ floatType ] false;
+ add "log1pl" longDoubleType [ longDoubleType ] false;
+
+ add "log2" doubleType [ doubleType ] false;
+ add "log2f" floatType [ floatType ] false;
+ add "log2l" longDoubleType [ longDoubleType ] false;
+
+ add "logb" doubleType [ doubleType ] false;
+ add "logbf" floatType [ floatType ] false;
+ add "logbl" longDoubleType [ longDoubleType ] false;
+
+ add "lrint" longType [ doubleType ] false;
+ add "lrintf" longType [ floatType ] false;
+ add "lrintl" longType [ longDoubleType ] false;
+
+ add "lround" longType [ doubleType ] false;
+ add "lroundf" longType [ floatType ] false;
+ add "lroundl" longType [ longDoubleType ] false;
+
+ add "memchr" voidPtrType [ voidConstPtrType; intType; sizeType ] false;
+ add "memcmp" intType [ voidConstPtrType; voidConstPtrType; sizeType ] false;
+ add "memcpy" voidPtrType [ voidPtrType; voidConstPtrType; sizeType ] false;
+ add "mempcpy" voidPtrType [ voidPtrType; voidConstPtrType; sizeType ] false;
+ add "memset" voidPtrType [ voidPtrType; intType; sizeType ] false;
+
+ add "modf" doubleType [ doubleType; TPtr(doubleType,[]) ] false;
+ add "modff" floatType [ floatType; TPtr(floatType,[]) ] false;
+ add "modfl"
+ longDoubleType [ longDoubleType; TPtr(longDoubleType, []) ] false;
+
+ add "nan" doubleType [ charConstPtrType ] false;
+ add "nanf" floatType [ charConstPtrType ] false;
+ add "nanl" longDoubleType [ charConstPtrType ] false;
+ add "nans" doubleType [ charConstPtrType ] false;
+ add "nansf" floatType [ charConstPtrType ] false;
+ add "nansl" longDoubleType [ charConstPtrType ] false;
+
+ add "nearbyint" doubleType [ doubleType ] false;
+ add "nearbyintf" floatType [ floatType ] false;
+ add "nearbyintl" longDoubleType [ longDoubleType ] false;
+
+ add "nextafter" doubleType [ doubleType; doubleType ] false;
+ add "nextafterf" floatType [ floatType; floatType ] false;
+ add "nextafterl" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "nexttoward" doubleType [ doubleType; longDoubleType ] false;
+ add "nexttowardf" floatType [ floatType; longDoubleType ] false;
+ add "nexttowardl" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "object_size" sizeType [ voidPtrType; intType ] false;
+
+ add "parity" intType [ uintType ] false;
+ add "parityl" intType [ ulongType ] false;
+ add "parityll" intType [ ulongLongType ] false;
+
+ add "pow" doubleType [ doubleType; doubleType ] false;
+ add "powf" floatType [ floatType; floatType ] false;
+ add "powl" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "powi" doubleType [ doubleType; intType ] false;
+ add "powif" floatType [ floatType; intType ] false;
+ add "powil" longDoubleType [ longDoubleType; intType ] false;
+
+ add "prefetch" voidType [ voidConstPtrType ] true;
+
+ add "printf" intType [ charConstPtrType ] true;
+ add "vprintf" intType [ charConstPtrType; TBuiltin_va_list [] ] false;
+ (* For [fprintf] and [vfprintf] the first argument is really FILE*, not void*,
+ but we don't want to build in the definition for FILE. *)
+ add "fprintf" intType [ voidPtrType; charConstPtrType ] true;
+ add "vfprintf"
+ intType [ voidPtrType; charConstPtrType; TBuiltin_va_list [] ] false;
+ add "sprintf" intType [ charPtrType; charConstPtrType ] true;
+ add "vsprintf"
+ intType [ charPtrType; charConstPtrType; TBuiltin_va_list [] ] false;
+ add "snprintf" intType [ charPtrType; sizeType; charConstPtrType ] true;
+ add "vsnprintf"
+ intType
+ [ charPtrType; sizeType; charConstPtrType; TBuiltin_va_list [] ]
+ false;
+
+ add "putchar" intType [ intType ] false;
+
+ add "puts" intType [ charConstPtrType ] false;
+ (* The second argument of [fputs] is really FILE*, not void*, but we
+ don't want to build in the definition for FILE. *)
+ add "fputs" intType [ charConstPtrType; voidPtrType ] false;
+
+ add "remainder" doubleType [ doubleType; doubleType ] false;
+ add "remainderf" floatType [ floatType; floatType ] false;
+ add "remainderl" longDoubleType [ longDoubleType; longDoubleType ] false;
+
+ add "remquo" doubleType [ doubleType; doubleType; intPtrType ] false;
+ add "remquof" floatType [ floatType; floatType; intPtrType ] false;
+ add "remquol"
+ longDoubleType [ longDoubleType; longDoubleType; intPtrType ] false;
+
+ add "return" voidType [ voidConstPtrType ] false;
+ add "return_address" voidPtrType [ uintType ] false;
+
+ add "rint" doubleType [ doubleType ] false;
+ add "rintf" floatType [ floatType ] false;
+ add "rintl" longDoubleType [ longDoubleType ] false;
+
+ add "round" doubleType [ doubleType ] false;
+ add "roundf" floatType [ floatType ] false;
+ add "roundl" longDoubleType [ longDoubleType ] false;
+
+ add "scalbln" doubleType [ doubleType; longType ] false;
+ add "scalblnf" floatType [ floatType; longType ] false;
+ add "scalblnl" longDoubleType [ longDoubleType; longType ] false;
+
+ add "scalbn" doubleType [ doubleType; intType ] false;
+ add "scalbnf" floatType [ floatType; intType ] false;
+ add "scalbnl" longDoubleType [ longDoubleType; intType ] false;
+
+ add "scanf" intType [ charConstPtrType ] true;
+ add "vscanf" intType [ charConstPtrType; TBuiltin_va_list [] ] false;
+ (* For [fscanf] and [vfscanf] the first argument is really FILE*, not void*,
+ but we don't want to build in the definition for FILE. *)
+ add "fscanf" intType [ voidPtrType; charConstPtrType ] true;
+ add "vfscanf"
+ intType [ voidPtrType; charConstPtrType; TBuiltin_va_list [] ] false;
+ add "sscanf" intType [ charConstPtrType; charConstPtrType ] true;
+ add "vsscanf"
+ intType [ charConstPtrType; charConstPtrType; TBuiltin_va_list [] ] false;
+
+ add "sin" doubleType [ doubleType ] false;
+ add "sinf" floatType [ floatType ] false;
+ add "sinl" longDoubleType [ longDoubleType ] false;
+
+ add "sinh" doubleType [ doubleType ] false;
+ add "sinhf" floatType [ floatType ] false;
+ add "sinhl" longDoubleType [ longDoubleType ] false;
+
+ add "sqrt" doubleType [ doubleType ] false;
+ add "sqrtf" floatType [ floatType ] false;
+ add "sqrtl" longDoubleType [ longDoubleType ] false;
+
+ add "stpcpy" charPtrType [ charPtrType; charConstPtrType ] false;
+ add "strcat" charPtrType [ charPtrType; charConstPtrType ] false;
+ add "strchr" charPtrType [ charPtrType; intType ] false;
+ add "strcmp" intType [ charConstPtrType; charConstPtrType ] false;
+ add "strcpy" charPtrType [ charPtrType; charConstPtrType ] false;
+ add "strcspn" sizeType [ charConstPtrType; charConstPtrType ] false;
+ add "strlen" sizeType [ charConstPtrType ] false;
+ add "strncat" charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
+ add "strncmp" intType [ charConstPtrType; charConstPtrType; sizeType ] false;
+ add "strncpy" charPtrType [ charPtrType; charConstPtrType; sizeType ] false;
+ add "strspn" sizeType [ charConstPtrType; charConstPtrType ] false;
+ add "strpbrk" charPtrType [ charConstPtrType; charConstPtrType ] false;
+ add "strrchr" charPtrType [ charConstPtrType; intType ] false;
+ add "strstr" charPtrType [ charConstPtrType; charConstPtrType ] false;
+ (* When we parse builtin_types_compatible_p, we change its interface *)
+ add "types_compatible_p"
+ intType
+ [ Cil.theMachine.typeOfSizeOf;(* Sizeof the type *)
+ Cil.theMachine.typeOfSizeOf (* Sizeof the type *) ]
+ false;
+ add "tan" doubleType [ doubleType ] false;
+ add "tanf" floatType [ floatType ] false;
+ add "tanl" longDoubleType [ longDoubleType ] false;
+
+ add "tanh" doubleType [ doubleType ] false;
+ add "tanhf" floatType [ floatType ] false;
+ add "tanhl" longDoubleType [ longDoubleType ] false;
+
+ add "tgamma" doubleType [ doubleType ] false;
+ add "tgammaf" floatType [ floatType ] false;
+ add "tgammal" longDoubleType [ longDoubleType ] false;
+
+ add "tolower" intType [ intType ] false;
+ add "toupper" intType [ intType ] false;
+
+ add "trunc" doubleType [ doubleType ] false;
+ add "truncf" floatType [ floatType ] false;
+ add "truncl" longDoubleType [ longDoubleType ] false;
+
+ add "unreachable" voidType [ ] false;
+
+ let int8_t = Some Cil.scharType in
+ let int16_t = try Some (Cil.int16_t ()) with Not_found -> None in
+ let int32_t = try Some (Cil.int32_t ()) with Not_found -> None in
+ let int64_t = try Some (Cil.int64_t ()) with Not_found -> None in
+ let uint8_t = Some Cil.ucharType in
+ let uint16_t = try Some (Cil.uint16_t ()) with Not_found -> None in
+ let uint32_t = try Some (Cil.uint32_t ()) with Not_found -> None in
+ let uint64_t = try Some (Cil.uint64_t ()) with Not_found -> None in
+
+ (* Binary monomorphic versions of atomic builtins *)
+ let atomic_instances =
+ [int8_t, "_int8_t";
+ int16_t,"_int16_t";
+ int32_t,"_int32_t";
+ int64_t,"_int64_t";
+ uint8_t, "_uint8_t";
+ uint16_t,"_uint16_t";
+ uint32_t,"_uint32_t";
+ uint64_t,"_uint64_t"]
+ in
+ let add_sync (typ,name) f =
+ match typ with
+ | Some typ ->
+ add ~prefix:"__sync_" (f^name) typ [ TPtr(typeAddVolatile typ,[]); typ] true
+ | None -> ()
+ in
+ let add_sync f =
+ List.iter (fun typ -> add_sync typ f) atomic_instances
+ in
+ add_sync "fetch_and_add";
+ add_sync "fetch_and_sub";
+ add_sync "fetch_and_or";
+ add_sync "fetch_and_and";
+ add_sync "fetch_and_xor";
+ add_sync "fetch_and_nand";
+ add_sync "add_and_fetch";
+ add_sync "sub_and_fetch";
+ add_sync "or_and_fetch";
+ add_sync "and_and_fetch";
+ add_sync "xor_and_fetch";
+ add_sync "nand_and_fetch";
+ add_sync "lock_test_and_set";
+ List.iter (fun (typ,n) ->
+ match typ with
+ | Some typ ->
+ add ~prefix:"" ("__sync_bool_compare_and_swap"^n)
+ intType
+ [ TPtr(typeAddVolatile typ,[]); typ ; typ]
+ true
+ | None -> ())
+ atomic_instances;
+ List.iter (fun (typ,n) ->
+ match typ with
+ | Some typ ->
+ add ~prefix:"" ("__sync_val_compare_and_swap"^n)
+ typ
+ [ TPtr(typeAddVolatile typ,[]); typ ; typ]
+ true
+ | None -> ())
+ atomic_instances;
+ List.iter (fun (typ,n) ->
+ match typ with
+ | Some typ ->
+ add ~prefix:"" ("__sync_lock_release"^n)
+ voidType
+ [ TPtr(typeAddVolatile typ,[]) ]
+ true;
+ | None -> ())
+ atomic_instances;
+ add ~prefix:"" "__sync_synchronize" voidType [] true
+;;
+
+(* Builtins related to va_list. Added to all non-msvc machdeps, because
+ Cabs2cil supposes they exist. *)
+let initVABuiltins () =
+ let hasbva = Cil.theMachine.theMachine.has__builtin_va_list in
+ let add = add_builtin in
+ add "next_arg"
+ (* When we parse builtin_next_arg we drop the second argument *)
+ (if hasbva then TBuiltin_va_list [] else voidPtrType) [] false;
+ if hasbva then begin
+ add "va_end" voidType [ TBuiltin_va_list [] ] false;
+ add "varargs_start" voidType [ TBuiltin_va_list [] ] false;
+ (* When we parse builtin_{va,stdarg}_start, we drop the second argument *)
+ add "va_start" voidType [ TBuiltin_va_list [] ] false;
+ add "stdarg_start" voidType [ TBuiltin_va_list [] ] false;
+ (* When we parse builtin_va_arg we change its interface *)
+ add "va_arg"
+ voidType
+ [ TBuiltin_va_list [];
+ Cil.theMachine.typeOfSizeOf;(* Sizeof the type *)
+ voidPtrType (* Ptr to res *) ]
+ false;
+ add "va_copy" voidType [ TBuiltin_va_list []; TBuiltin_va_list [] ] false;
+ end
+
+let initMsvcBuiltins () : unit =
+ (** Take a number of wide string literals *)
+ Builtin_functions.add "__annotation" (voidType, [ ], true)
+
+let init_common_builtins () =
+ add_builtin
+ "offsetof"
+ Cil.theMachine.typeOfSizeOf
+ [ Cil.theMachine.typeOfSizeOf ]
+ false
+
+let init_builtins () =
+ if not (Cil.selfMachine_is_computed ()) then
+ Kernel.fatal ~current:true "You must call initCIL before init_builtins" ;
+ if Builtin_functions.length () <> 0 then
+ Kernel.fatal ~current:true "Cil builtins already initialized." ;
+ init_common_builtins ();
+ if Cil.msvcMode () then
+ initMsvcBuiltins ()
+ else begin
+ initVABuiltins ();
+ if Cil.gccMode () then initGccBuiltins ();
+ end
+
+(** This is used as the location of the prototypes of builtin functions. *)
+let builtinLoc: location = Location.unknown
+
+let () =
+ Cil.init_builtins_ref := init_builtins
diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli
new file mode 100644
index 0000000000000000000000000000000000000000..adb9caf1eb57e165b9e9ba0d56d9bf8e9dce3670
--- /dev/null
+++ b/src/kernel_services/ast_queries/cil_builtins.mli
@@ -0,0 +1,98 @@
+(****************************************************************************)
+(* *)
+(* Copyright (C) 2001-2003 *)
+(* George C. Necula <necula@cs.berkeley.edu> *)
+(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
+(* Wes Weimer <weimer@cs.berkeley.edu> *)
+(* Ben Liblit <liblit@cs.berkeley.edu> *)
+(* All rights reserved. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in the *)
+(* documentation and/or other materials provided with the distribution. *)
+(* *)
+(* 3. The names of the contributors may not be used to endorse or *)
+(* promote products derived from this software without specific prior *)
+(* written permission. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
+(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
+(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
+(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
+(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
+(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
+(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
+(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
+(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
+(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
+(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
+(* POSSIBILITY OF SUCH DAMAGE. *)
+(* *)
+(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
+(* énergies alternatives) *)
+(* and INRIA (Institut National de Recherche en Informatique *)
+(* et Automatique). *)
+(****************************************************************************)
+
+open Cil_types
+
+(* ************************************************************************* *)
+(** {2 Builtins management} *)
+(* ************************************************************************* *)
+
+(** This module associates the name of a built-in function that might be used
+ during elaboration with the corresponding varinfo. This is done when
+ parsing ${FRAMAC_SHARE}/libc/__fc_builtins.h, which is always performed
+ before processing the actual list of files provided on the command line (see
+ {!File.init_from_c_files}). Actual list of such built-ins is managed in
+ {!Cabs2cil}. *)
+module Frama_c_builtins:
+ State_builder.Hashtbl with type key = string and type data = varinfo
+
+val is_builtin: varinfo -> bool
+(** @return true if the given variable refers to a Frama-C builtin.
+ @since Fluorine-20130401 *)
+
+val is_unused_builtin: varinfo -> bool
+(** @return true if the given variable refers to a Frama-C builtin that
+ is not used in the current program. Plugins may (and in fact should)
+ hide this builtin from their outputs *)
+
+val is_special_builtin: string -> bool
+(** @return [true] if the given name refers to a special built-in function.
+ A special built-in function can have any number of arguments. It is up to
+ the plug-ins to know what to do with it.
+ @since Carbon-20101201 *)
+
+(** register a new special built-in function *)
+val add_special_builtin: string -> unit
+
+(** register a new family of special built-in functions.
+ @since Carbon-20101201
+*)
+val add_special_builtin_family: (string -> bool) -> unit
+
+(** initialize the C built-ins. Should be called once per project, after the
+ machine has been set. *)
+val init_builtins: unit -> unit
+
+(** A list of the built-in functions for the current compiler (GCC or
+ * MSVC, depending on [!msvcMode]). Maps the name to the
+ * result and argument types, and whether it is vararg.
+ * Initialized by {!Cil.initCIL}
+ *
+ * This map replaces [gccBuiltins] and [msvcBuiltins] in previous
+ * versions of CIL.*)
+module Builtin_functions :
+ State_builder.Hashtbl with type key = string
+ and type data = typ * typ list * bool
+
+(** This is used as the location of the prototypes of builtin functions. *)
+val builtinLoc: location
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 4884c022eaee34b73c4d10a918b39da902856915..c09cbcdf03392984aea89aba2f3ec7e13ccef2d0 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -208,7 +208,7 @@ end = struct
[ Ast.self;
Ast.UntypedFiles.self;
Cabshelper.Comments.self;
- Cil.Frama_c_builtins.self ]
+ Cil_builtins.Frama_c_builtins.self ]
let () =
Ast.add_linked_state Cabshelper.Comments.self
@@ -1188,7 +1188,7 @@ let prepare_cil_file ast =
let fill_built_ins () =
if Cil.selfMachine_is_computed () then begin
Kernel.debug "Machine is computed, just fill the built-ins";
- Cil.init_builtins ();
+ Cil_builtins.init_builtins ();
end else begin
Kernel.debug "Machine is not computed, initialize everything";
Cil.initCIL (Logic_builtin.init()) (get_machdep ());
@@ -1203,7 +1203,7 @@ let init_project_from_cil_file prj file =
State_selection.full
(State_selection.list_union
(List.map State_selection.with_dependencies
- [Cil.Builtin_functions.self;
+ [Cil_builtins.Builtin_functions.self;
Ast.self;
Files.pre_register_state]))
in
@@ -1685,7 +1685,7 @@ let init_from_cmdline () =
let selection =
State_selection.list_union
(List.map State_selection.with_dependencies
- [ Cil.Builtin_functions.self;
+ [ Cil_builtins.Builtin_functions.self;
Logic_env.Logic_info.self;
Logic_env.Logic_type_info.self;
Logic_env.Logic_ctor_info.self;
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 9192bb4f790dddd6d5b6a5bf14b379616ee9b377..0498ef145a6f1abd70ada90149e8b6a92cfd1e54 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -31,23 +31,23 @@ type cpp_opt_kind = Gnu | Not_gnu | Unknown
names given on the command line, without normalization. *)
type file =
| NeedCPP of Filepath.Normalized.t * string * cpp_opt_kind
- (** The first string is the filename of the [.c] to preprocess.
- The second one is the preprocessor command ([filename.c -o
- tempfilname.i] will be appended at the end).*)
+ (** The first string is the filename of the [.c] to preprocess.
+ The second one is the preprocessor command ([filename.c -o
+ tempfilname.i] will be appended at the end).*)
| NoCPP of Filepath.Normalized.t
- (** Already pre-processed file [.i] *)
+ (** Already pre-processed file [.i] *)
| External of Filepath.Normalized.t * string
- (** file that can be translated into a Cil AST through an external
- function, together with the recognized suffix. *)
+ (** file that can be translated into a Cil AST through an external
+ function, together with the recognized suffix. *)
include Datatype.S with type t = file
val new_file_type:
string -> (string -> Cil_types.file * Cabs.file) -> unit
- (** [new_file_type suffix func funcname] registers a new type of files (with
- corresponding suffix) as recognized by Frama-C through [func].
- @plugin development guide
- *)
+(** [new_file_type suffix func funcname] registers a new type of files (with
+ corresponding suffix) as recognized by Frama-C through [func].
+ @plugin development guide
+*)
val new_machdep: string -> Cil_types.mach -> unit
(** [new_machdep name module] registers a new machdep name as recognized by
@@ -61,152 +61,152 @@ val new_machdep: string -> Cil_types.mach -> unit
@plugin development guide *)
val machdep_macro: string -> string
- (** [machdep_macro machine] returns the name of a macro __FC_MACHDEP_XXX so
- that the preprocessor can select std lib definition consistent with
- the selected machdep. This function will emit a warning if [machine] is
- not known by default by the kernel and return __FC_MACHDEP_MACHINE in that
- case.
- @since Magnesium-20151001 (exported in the API)
- *)
+(** [machdep_macro machine] returns the name of a macro __FC_MACHDEP_XXX so
+ that the preprocessor can select std lib definition consistent with
+ the selected machdep. This function will emit a warning if [machine] is
+ not known by default by the kernel and return __FC_MACHDEP_MACHINE in that
+ case.
+ @since Magnesium-20151001 (exported in the API)
+*)
val list_available_machdeps: unit -> string list
(** [list_available_machdeps ()] gives the list of the names of available
machdeps, starting with the ones added with new_machdep and ending with
the list of default machdeps.
@since 22.0-Titanium *)
-
+
type code_transformation_category
(** type of registered code transformations
- @since Neon-20140301
+ @since Neon-20140301
*)
val register_code_transformation_category:
string -> code_transformation_category
(** Adds a new category of code transformation *)
-val add_code_transformation_before_cleanup:
+val add_code_transformation_before_cleanup:
?deps:(module Parameter_sig.S) list ->
?before:code_transformation_category list ->
?after:code_transformation_category list ->
code_transformation_category -> (Cil_types.file -> unit) -> unit
- (** [add_code_transformation_before_cleanup name hook]
- adds an hook in the corresponding category
- that will be called during the normalization of a linked
- file, before clean up and removal of temps and unused declarations.
- If this transformation involves changing statements of a function [f],
- [f] must be flagged with {!File.must_recompute_cfg}.
- The optional [before] (resp [after]) categories indicates that current
- transformation must be executed before (resp after)
- the corresponding ones, if they exist. In case of dependencies cycle,
- an arbitrary order will be chosen for the transformations involved in
- the cycle.
- The optional [deps] argument gives the list of options whose change
- (e.g. after a [-then]) will trigger the transformation over the already
- computed AST. If several transformations are triggered by the same
- option, their relative order is preserved.
-
- At this level, globals and ACSL annotations have not been registered.
-
- @since Neon-20140301
- @plugin development guide *)
+(** [add_code_transformation_before_cleanup name hook]
+ adds an hook in the corresponding category
+ that will be called during the normalization of a linked
+ file, before clean up and removal of temps and unused declarations.
+ If this transformation involves changing statements of a function [f],
+ [f] must be flagged with {!File.must_recompute_cfg}.
+ The optional [before] (resp [after]) categories indicates that current
+ transformation must be executed before (resp after)
+ the corresponding ones, if they exist. In case of dependencies cycle,
+ an arbitrary order will be chosen for the transformations involved in
+ the cycle.
+ The optional [deps] argument gives the list of options whose change
+ (e.g. after a [-then]) will trigger the transformation over the already
+ computed AST. If several transformations are triggered by the same
+ option, their relative order is preserved.
+
+ At this level, globals and ACSL annotations have not been registered.
+
+ @since Neon-20140301
+ @plugin development guide *)
val add_code_transformation_after_cleanup:
?deps:(module Parameter_sig.S) list ->
?before:code_transformation_category list ->
?after:code_transformation_category list ->
code_transformation_category -> (Cil_types.file -> unit) -> unit
- (** Same as above, but the hook is applied after clean up.
- At this level, globals and ACSL annotations have been registered. If
- the hook adds some new globals or annotations, it must take care of
- adding them in the appropriate tables.
- Note that it is the responsibility of the hook to use
- {!Ast.mark_as_changed} or {!Ast.mark_as_grown} whenever it is the case.
- @since Neon-20140301
- @plugin development guide *)
+(** Same as above, but the hook is applied after clean up.
+ At this level, globals and ACSL annotations have been registered. If
+ the hook adds some new globals or annotations, it must take care of
+ adding them in the appropriate tables.
+ Note that it is the responsibility of the hook to use
+ {!Ast.mark_as_changed} or {!Ast.mark_as_grown} whenever it is the case.
+ @since Neon-20140301
+ @plugin development guide *)
val constfold: code_transformation_category
(** category for syntactic constfolding (done after cleanup)
@since Silicon-20161101 *)
val must_recompute_cfg: Cil_types.fundec -> unit
- (** [must_recompute_cfg f] must be called by code transformation hooks
- when they modify statements in function [f]. This will trigger a
- recomputation of the cfg of [f] after the transformation.
- @since Neon-20140301
- @plugin development guide *)
+(** [must_recompute_cfg f] must be called by code transformation hooks
+ when they modify statements in function [f]. This will trigger a
+ recomputation of the cfg of [f] after the transformation.
+ @since Neon-20140301
+ @plugin development guide *)
val get_suffixes: unit -> string list
- (** @return the list of accepted suffixes of input source files
- @since Boron-20100401 *)
+(** @return the list of accepted suffixes of input source files
+ @since Boron-20100401 *)
val get_name: t -> string
- (** File name (not normalized). *)
+(** File name (not normalized). *)
val get_preprocessor_command: unit -> string * cpp_opt_kind
- (** Return the preprocessor command to use. *)
+(** Return the preprocessor command to use. *)
val pre_register: t -> unit
- (** Register some file as source file before command-line files *)
+(** Register some file as source file before command-line files *)
val get_all: unit -> t list
- (** Return the list of toplevel files. *)
+(** Return the list of toplevel files. *)
val from_filename: ?cpp:string -> Datatype.Filepath.t -> t
- (** Build a file from its name. The optional argument is the preprocessor
- command. Default is [!get_preprocessor_command ()]. *)
+(** Build a file from its name. The optional argument is the preprocessor
+ command. Default is [!get_preprocessor_command ()]. *)
(* ************************************************************************* *)
(** {2 Initializers} *)
(* ************************************************************************* *)
val prepare_from_c_files: unit -> unit
- (** Initialize the AST of the current project according to the current
- filename list.
- @raise File_types.Bad_Initialization if called more than once. *)
+(** Initialize the AST of the current project according to the current
+ filename list.
+ @raise File_types.Bad_Initialization if called more than once. *)
val init_from_c_files: t list -> unit
- (** Initialize the cil file representation of the current project.
- Should be called at most once per project.
- @raise File_types.Bad_Initialization if called more than once.
- @plugin development guide *)
+(** Initialize the cil file representation of the current project.
+ Should be called at most once per project.
+ @raise File_types.Bad_Initialization if called more than once.
+ @plugin development guide *)
val init_project_from_cil_file: Project.t -> Cil_types.file -> unit
- (** Initialize the cil file representation with the given file for the
- given project from the current one.
- Should be called at most once per project.
- @raise File_types.Bad_Initialization if called more than once.
- @plugin development guide *)
+(** Initialize the cil file representation with the given file for the
+ given project from the current one.
+ Should be called at most once per project.
+ @raise File_types.Bad_Initialization if called more than once.
+ @plugin development guide *)
val init_project_from_visitor:
?reorder:bool -> Project.t -> Visitor.frama_c_visitor -> unit
- (** [init_project_from_visitor prj vis] initialize the cil file
- representation of [prj]. [prj] must be essentially empty: it can have
- some options set, but not an existing cil file; [proj] is filled using
- [vis], which must be a copy visitor that puts its results in [prj].
- if [reorder] is [true] (default is [false]) the new AST in [prj]
- will be reordered.
- @since Oxygen-20120901
- @modify Fluorine-20130401 added reorder optional argument
- @plugin development guide
- *)
+(** [init_project_from_visitor prj vis] initialize the cil file
+ representation of [prj]. [prj] must be essentially empty: it can have
+ some options set, but not an existing cil file; [proj] is filled using
+ [vis], which must be a copy visitor that puts its results in [prj].
+ if [reorder] is [true] (default is [false]) the new AST in [prj]
+ will be reordered.
+ @since Oxygen-20120901
+ @modify Fluorine-20130401 added reorder optional argument
+ @plugin development guide
+*)
val create_project_from_visitor:
?reorder:bool -> ?last:bool ->
string ->
(Project.t -> Visitor.frama_c_visitor) ->
Project.t
- (** Return a new project with a new cil file representation by visiting the
- file of the current project. If [reorder] is [true], the globals in the
- AST of the new project are reordered (default is [false]). If [last] is
- [true] (by default), remember than the returned project is the last
- created one.
- The visitor is responsible to avoid sharing between old file and new
- file (i.e. it should use {!Cil.copy_visit} at some point).
- @raise File_types.Bad_Initialization if called more than once.
- @since Beryllium-20090601-beta1
- @modify Fluorine-20130401 added [reorder] optional argument
- @modify Sodium-20150201 added [last] optional argument
- @plugin development guide *)
+(** Return a new project with a new cil file representation by visiting the
+ file of the current project. If [reorder] is [true], the globals in the
+ AST of the new project are reordered (default is [false]). If [last] is
+ [true] (by default), remember than the returned project is the last
+ created one.
+ The visitor is responsible to avoid sharing between old file and new
+ file (i.e. it should use {!Cil.copy_visit} at some point).
+ @raise File_types.Bad_Initialization if called more than once.
+ @since Beryllium-20090601-beta1
+ @modify Fluorine-20130401 added [reorder] optional argument
+ @modify Sodium-20150201 added [last] optional argument
+ @plugin development guide *)
val create_rebuilt_project_from_visitor:
?reorder:bool -> ?last:bool -> ?preprocess:bool ->
@@ -221,7 +221,7 @@ val create_rebuilt_project_from_visitor:
NOT preprocessed by default.
@raise File_types.Bad_Initialization if called more than once.
- @since Nitrogen-20111001
+ @since Nitrogen-20111001
@modify Fluorine-20130401 added reorder optional argument
*)
@@ -236,10 +236,10 @@ val init_from_cmdline: unit -> unit
@plugin development guide *)
val reorder_ast: unit -> unit
- (** reorder globals so that all uses of an identifier are preceded by its
- declaration. This may introduce new declarations in the AST.
- @since Oxygen-20120901
- *)
+(** reorder globals so that all uses of an identifier are preceded by its
+ declaration. This may introduce new declarations in the AST.
+ @since Oxygen-20120901
+*)
val reorder_custom_ast: Cil_types.file -> unit
(** @since Neon-20140301 *)
@@ -250,14 +250,14 @@ val reorder_custom_ast: Cil_types.file -> unit
val pretty_machdep :
?fmt:Format.formatter -> ?machdep:Cil_types.mach -> unit -> unit
- (** Prints the associated [machdep], or the current one in current project
- by default. Default output formatter is [Log.print_on_output]. *)
+(** Prints the associated [machdep], or the current one in current project
+ by default. Default output formatter is [Log.print_on_output]. *)
val pretty_ast : ?prj:Project.t -> ?fmt:Format.formatter -> unit -> unit
- (** Print the project CIL file on the given Formatter.
- The default project is the current one.
- The default formatter is [Kernel.CodeOutput.get_fmt ()].
- @raise File_types.Bad_Initialization if the file is not initialized. *)
+(** Print the project CIL file on the given Formatter.
+ The default project is the current one.
+ The default formatter is [Kernel.CodeOutput.get_fmt ()].
+ @raise File_types.Bad_Initialization if the file is not initialized. *)
(*
Local Variables:
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index cc918e122f511db3fe8acf500aaaa9c701204b9f..5e70d27b1772c1cc0f4eb9d0761cff7855b43043 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -48,790 +48,790 @@ end
annotations may not be visited properly. *)
class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c_visitor =
-object(self)
- inherit internal_genericCilVisitor fundec behavior queue
+ object(self)
+ inherit internal_genericCilVisitor fundec behavior queue
- method frama_c_plain_copy =
- new internal_generic_frama_c_visitor fundec queue current_kf behavior
+ method frama_c_plain_copy =
+ new internal_generic_frama_c_visitor fundec queue current_kf behavior
- method! plain_copy_visitor =
- assert (self#frama_c_plain_copy#get_filling_actions ==
+ method! plain_copy_visitor =
+ assert (self#frama_c_plain_copy#get_filling_actions ==
self#get_filling_actions);
- (self#frama_c_plain_copy :> Cil.cilVisitor)
-
- method set_current_kf kf = current_kf := Some kf
-
- method reset_current_kf () = current_kf := None
-
- method current_kf = !current_kf
-
- method! private vstmt stmt =
- let orig_stmt = Visitor_behavior.Get_orig.stmt self#behavior stmt in
- let annots =
- Annotations.fold_code_annot (fun e a acc -> (e, a) :: acc) orig_stmt []
- in
- let res = self#vstmt_aux stmt in
- (* Annotations will be visited and more importantly added in the
- same order as they were in the original AST. *)
- let annots =
- List.sort
- (fun (_,a) (_,b) -> Cil_datatype.Code_annotation.compare a b)
- annots
- in
- let make_children_annot vis =
- let add, remove =
- List.fold_left
- (fun (add, remove) (e, x) ->
- let y = visitCilCodeAnnotation (vis:>cilVisitor) x in
- (* Given x, we compute whether it must be removed from the
- destination project, and whether we should add its copy y,
- again in the destination project. *)
- let is_trivial = Logic_utils.is_trivial_annotation in
- (* we keep [y] only if it is non-trivial (non-\true), except
- if [x] is already trivial itself. *)
- let becomes_trivial = is_trivial y && not (is_trivial x) in
- let curr_add, remove_curr =
- if Visitor_behavior.is_copy vis#behavior then
- (* Copy visitor. We add [y], except if trivial. No sense in
- removing [x], since the stmt is a new one. *)
- (if not becomes_trivial then [e, y] else []),
- false
- else
- (* Inplace visitor. We remove [x] if it becomes trivial, or
- if it has changed (because we need to add it back with the
- new content). We re-add [y] if [x] has changed and has
- not became trivial. Do not always remove then re-add, as
- this would mess up property statuses. *)
- (if x != y && not becomes_trivial then [e, y] else []),
- (x != y || becomes_trivial)
- in
- (add @ curr_add, if remove_curr then (e, x) :: remove else remove)
- )
- ([],[])
+ (self#frama_c_plain_copy :> Cil.cilVisitor)
+
+ method set_current_kf kf = current_kf := Some kf
+
+ method reset_current_kf () = current_kf := None
+
+ method current_kf = !current_kf
+
+ method! private vstmt stmt =
+ let orig_stmt = Visitor_behavior.Get_orig.stmt self#behavior stmt in
+ let annots =
+ Annotations.fold_code_annot (fun e a acc -> (e, a) :: acc) orig_stmt []
+ in
+ let res = self#vstmt_aux stmt in
+ (* Annotations will be visited and more importantly added in the
+ same order as they were in the original AST. *)
+ let annots =
+ List.sort
+ (fun (_,a) (_,b) -> Cil_datatype.Code_annotation.compare a b)
annots
in
- (add, remove)
- in
- let change_stmt stmt (add, remove) =
- if (add <> [] || remove <> []) then begin
- let kf = Extlib.the self#current_kf in
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- Queue.add
- (fun () ->
- List.iter
- (fun (e, a) ->
- Annotations.remove_code_annot e ~kf:new_kf stmt a)
- remove;
- List.iter
- (fun (e, a) ->
- Annotations.add_code_annot
- ~keep_empty:false e ~kf:new_kf stmt a)
- add)
- self#get_filling_actions
- end
- in
- let post_action f stmt =
- let (add, _ as new_annots) = make_children_annot self in
- let stmt = f stmt in
- (match stmt.skind with
- | Block b when annots <> [] || add <> [] ->
- stmt.skind <- Block (Cil.block_of_transient b)
- | _ -> ());
- change_stmt stmt new_annots;
- stmt
- in
- let copy stmt =
- change_stmt stmt(make_children_annot self#frama_c_plain_copy);
- stmt
- in
- let plain_post = post_action (fun x -> x) in
- match res with
- | SkipChildren -> res
- | JustCopy -> JustCopyPost copy
- | JustCopyPost f -> JustCopyPost (f $ copy)
- | DoChildren -> DoChildrenPost plain_post
- | DoChildrenPost f -> DoChildrenPost (f $ plain_post)
- | ChangeTo _ | ChangeToPost _ -> res
- | ChangeDoChildrenPost (stmt,f) ->
- ChangeDoChildrenPost (stmt, post_action f)
-
- method vstmt_aux _ = DoChildren
- method vglob_aux _ = DoChildren
-
- method private vbehavior_annot ?e b =
- let kf = Extlib.the self#current_kf in
- let treat_elt emit elt acc =
- match e with
+ let make_children_annot vis =
+ let add, remove =
+ List.fold_left
+ (fun (add, remove) (e, x) ->
+ let y = visitCilCodeAnnotation (vis:>cilVisitor) x in
+ (* Given x, we compute whether it must be removed from the
+ destination project, and whether we should add its copy y,
+ again in the destination project. *)
+ let is_trivial = Logic_utils.is_trivial_annotation in
+ (* we keep [y] only if it is non-trivial (non-\true), except
+ if [x] is already trivial itself. *)
+ let becomes_trivial = is_trivial y && not (is_trivial x) in
+ let curr_add, remove_curr =
+ if Visitor_behavior.is_copy vis#behavior then
+ (* Copy visitor. We add [y], except if trivial. No sense in
+ removing [x], since the stmt is a new one. *)
+ (if not becomes_trivial then [e, y] else []),
+ false
+ else
+ (* Inplace visitor. We remove [x] if it becomes trivial, or
+ if it has changed (because we need to add it back with the
+ new content). We re-add [y] if [x] has changed and has
+ not became trivial. Do not always remove then re-add, as
+ this would mess up property statuses. *)
+ (if x != y && not becomes_trivial then [e, y] else []),
+ (x != y || becomes_trivial)
+ in
+ (add @ curr_add, if remove_curr then (e, x) :: remove else remove)
+ )
+ ([],[])
+ annots
+ in
+ (add, remove)
+ in
+ let change_stmt stmt (add, remove) =
+ if (add <> [] || remove <> []) then begin
+ let kf = Extlib.the self#current_kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ Queue.add
+ (fun () ->
+ List.iter
+ (fun (e, a) ->
+ Annotations.remove_code_annot e ~kf:new_kf stmt a)
+ remove;
+ List.iter
+ (fun (e, a) ->
+ Annotations.add_code_annot
+ ~keep_empty:false e ~kf:new_kf stmt a)
+ add)
+ self#get_filling_actions
+ end
+ in
+ let post_action f stmt =
+ let (add, _ as new_annots) = make_children_annot self in
+ let stmt = f stmt in
+ (match stmt.skind with
+ | Block b when annots <> [] || add <> [] ->
+ stmt.skind <- Block (Cil.block_of_transient b)
+ | _ -> ());
+ change_stmt stmt new_annots;
+ stmt
+ in
+ let copy stmt =
+ change_stmt stmt(make_children_annot self#frama_c_plain_copy);
+ stmt
+ in
+ let plain_post = post_action (fun x -> x) in
+ match res with
+ | SkipChildren -> res
+ | JustCopy -> JustCopyPost copy
+ | JustCopyPost f -> JustCopyPost (f $ copy)
+ | DoChildren -> DoChildrenPost plain_post
+ | DoChildrenPost f -> DoChildrenPost (f $ plain_post)
+ | ChangeTo _ | ChangeToPost _ -> res
+ | ChangeDoChildrenPost (stmt,f) ->
+ ChangeDoChildrenPost (stmt, post_action f)
+
+ method vstmt_aux _ = DoChildren
+ method vglob_aux _ = DoChildren
+
+ method private vbehavior_annot ?e b =
+ let kf = Extlib.the self#current_kf in
+ let treat_elt emit elt acc =
+ match e with
| None -> (emit, elt) :: acc
| Some e when Emitter.equal e emit -> (emit, elt) :: acc
| Some _ -> acc
- in
- let fold_elt fold = fold treat_elt kf b.b_name [] in
- let old_requires = fold_elt Annotations.fold_requires in
- let old_assumes = fold_elt Annotations.fold_assumes in
- let old_ensures = fold_elt Annotations.fold_ensures in
- let old_assigns = fold_elt Annotations.fold_assigns in
- let old_allocates = fold_elt Annotations.fold_allocates in
- let old_extended = fold_elt Annotations.fold_extended in
- let b' =
- if Visitor_behavior.is_copy self#behavior then
- { b with b_name = b.b_name }
- else b
- in
- let res = self#vbehavior b' in
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- let add_queue a = Queue.add a self#get_filling_actions in
- let visit_clauses vis f =
- (* Ensures that we have a table associated to new_kf in Annotations. *)
- add_queue
- (fun () ->
- ignore (Annotations.behaviors ~populate:false new_kf));
- let module Fold =
- struct
- type 'a t =
- { apply: 'b. (Emitter.t -> 'a -> 'b -> 'b) ->
- Kernel_function.t -> string -> 'b -> 'b }
- end
in
- let visit_elt visit e elt (f,acc) =
- let new_elt = visit (vis:>Cil.cilVisitor) elt in
- (* We'll add the elts afterwards, so as to keep lists in their
- original order as much as we can. see fold_elt below.
- *)
- f || new_elt != elt || new_kf != kf,
- (e,new_elt) :: acc
+ let fold_elt fold = fold treat_elt kf b.b_name [] in
+ let old_requires = fold_elt Annotations.fold_requires in
+ let old_assumes = fold_elt Annotations.fold_assumes in
+ let old_ensures = fold_elt Annotations.fold_ensures in
+ let old_assigns = fold_elt Annotations.fold_assigns in
+ let old_allocates = fold_elt Annotations.fold_allocates in
+ let old_extended = fold_elt Annotations.fold_extended in
+ let b' =
+ if Visitor_behavior.is_copy self#behavior then
+ { b with b_name = b.b_name }
+ else b
in
- let check_elt visit e' elt acc =
- match e with
+ let res = self#vbehavior b' in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ let add_queue a = Queue.add a self#get_filling_actions in
+ let visit_clauses vis f =
+ (* Ensures that we have a table associated to new_kf in Annotations. *)
+ add_queue
+ (fun () ->
+ ignore (Annotations.behaviors ~populate:false new_kf));
+ let module Fold =
+ struct
+ type 'a t =
+ { apply: 'b. (Emitter.t -> 'a -> 'b -> 'b) ->
+ Kernel_function.t -> string -> 'b -> 'b }
+ end
+ in
+ let visit_elt visit e elt (f,acc) =
+ let new_elt = visit (vis:>Cil.cilVisitor) elt in
+ (* We'll add the elts afterwards, so as to keep lists in their
+ original order as much as we can. see fold_elt below.
+ *)
+ f || new_elt != elt || new_kf != kf,
+ (e,new_elt) :: acc
+ in
+ let check_elt visit e' elt acc =
+ match e with
| None -> visit_elt visit e' elt acc
| Some e when Emitter.equal e e' -> visit_elt visit e' elt acc
| Some _ -> acc
- in
- let fold_elt fold visit remove add append dft =
- let (changed, res) =
- fold.Fold.apply (check_elt visit) kf b'.b_name (false,[])
in
- if changed then begin
- add_queue
- (fun () ->
- fold.Fold.apply
- (fun e' x () ->
- match e with
- | None -> remove e' new_kf x
- | Some e when Emitter.equal e e' -> remove e' new_kf x
- | _ -> ())
- new_kf b'.b_name ();
- List.iter (fun (e,x) -> add e new_kf b'.b_name x) res)
- end;
- List.fold_left (fun acc (_,x) -> append x acc) dft res
- in
- let req =
- fold_elt
- { Fold.apply = Annotations.fold_requires }
- Cil.visitCilIdPredicate
- Annotations.remove_requires
- (fun e kf behavior r -> Annotations.add_requires e kf ~behavior [r])
- (fun x l -> x :: l) []
- in
- b'.b_requires <- req;
- let assumes =
- fold_elt
- { Fold.apply = Annotations.fold_assumes }
- Cil.visitCilIdPredicate
- Annotations.remove_assumes
- (fun e kf behavior a -> Annotations.add_assumes e kf ~behavior [a])
- (fun x l -> x :: l) []
- in
- b'.b_assumes <- assumes;
- let visit_ensures vis (k,p as e) =
- let new_p = Cil.visitCilIdPredicate (vis:>Cil.cilVisitor) p in
- if p != new_p then (k,new_p) else e
- in
- let ensures =
- fold_elt
- { Fold.apply = Annotations.fold_ensures }
- visit_ensures
- Annotations.remove_ensures
- (fun e kf behavior p -> Annotations.add_ensures e kf ~behavior [p])
- (fun x l -> x :: l) []
- in
- b'.b_post_cond <- ensures;
- let add_assigns e kf behavior a =
- match a with
+ let fold_elt fold visit remove add append dft =
+ let (changed, res) =
+ fold.Fold.apply (check_elt visit) kf b'.b_name (false,[])
+ in
+ if changed then begin
+ add_queue
+ (fun () ->
+ fold.Fold.apply
+ (fun e' x () ->
+ match e with
+ | None -> remove e' new_kf x
+ | Some e when Emitter.equal e e' -> remove e' new_kf x
+ | _ -> ())
+ new_kf b'.b_name ();
+ List.iter (fun (e,x) -> add e new_kf b'.b_name x) res)
+ end;
+ List.fold_left (fun acc (_,x) -> append x acc) dft res
+ in
+ let req =
+ fold_elt
+ { Fold.apply = Annotations.fold_requires }
+ Cil.visitCilIdPredicate
+ Annotations.remove_requires
+ (fun e kf behavior r -> Annotations.add_requires e kf ~behavior [r])
+ (fun x l -> x :: l) []
+ in
+ b'.b_requires <- req;
+ let assumes =
+ fold_elt
+ { Fold.apply = Annotations.fold_assumes }
+ Cil.visitCilIdPredicate
+ Annotations.remove_assumes
+ (fun e kf behavior a -> Annotations.add_assumes e kf ~behavior [a])
+ (fun x l -> x :: l) []
+ in
+ b'.b_assumes <- assumes;
+ let visit_ensures vis (k,p as e) =
+ let new_p = Cil.visitCilIdPredicate (vis:>Cil.cilVisitor) p in
+ if p != new_p then (k,new_p) else e
+ in
+ let ensures =
+ fold_elt
+ { Fold.apply = Annotations.fold_ensures }
+ visit_ensures
+ Annotations.remove_ensures
+ (fun e kf behavior p -> Annotations.add_ensures e kf ~behavior [p])
+ (fun x l -> x :: l) []
+ in
+ b'.b_post_cond <- ensures;
+ let add_assigns e kf behavior a =
+ match a with
| WritesAny -> ()
| _ -> Annotations.add_assigns ~keep_empty:false e kf ~behavior a
- in
- let concat_assigns new_a a =
- match new_a, a with
+ in
+ let concat_assigns new_a a =
+ match new_a, a with
| WritesAny, a | a, WritesAny -> a
| Writes a1, Writes a2 -> Writes (a2 @ a1)
- in
- let a =
- fold_elt
- { Fold.apply = Annotations.fold_assigns }
- Cil.visitCilAssigns
- Annotations.remove_assigns
- add_assigns
- concat_assigns
- WritesAny
- in
- b'.b_assigns <- a;
- let concat_allocation new_a a =
- match new_a, a with
+ in
+ let a =
+ fold_elt
+ { Fold.apply = Annotations.fold_assigns }
+ Cil.visitCilAssigns
+ Annotations.remove_assigns
+ add_assigns
+ concat_assigns
+ WritesAny
+ in
+ b'.b_assigns <- a;
+ let concat_allocation new_a a =
+ match new_a, a with
| FreeAllocAny, a | a, FreeAllocAny -> a
| FreeAlloc(a1,a2), FreeAlloc(a3,a4) -> FreeAlloc (a3@a1,a4@a2)
+ in
+ let a =
+ fold_elt
+ { Fold.apply = Annotations.fold_allocates }
+ Cil.visitCilAllocation
+ Annotations.remove_allocates
+ (fun e kf behavior a ->
+ Annotations.add_allocates ~keep_empty:false e kf ~behavior a)
+ concat_allocation
+ FreeAllocAny
+ in
+ b'.b_allocation <- a;
+ let ext =
+ fold_elt
+ { Fold.apply = Annotations.fold_extended }
+ Cil.visitCilExtended
+ Annotations.remove_extended
+ (fun e kf behavior ex -> Annotations.add_extended e kf ~behavior ex)
+ (fun x y -> x::y)
+ []
+ in
+ b'.b_extended <- ext;
+ f b'
+ in
+ let remove_and_add get remove add fold old b =
+ let emitter = match e with None -> Emitter.end_user | Some e -> e in
+ let elts = get b in
+ List.iter
+ (fun (e,x) ->
+ if not (List.memq x elts) then
+ add_queue (fun () -> remove e new_kf x))
+ old;
+ let module M = struct exception Found of Emitter.t end in
+ let already_there x =
+ fold (fun e y () -> if x == y then raise (M.Found e)) new_kf b.b_name ()
+ in
+ List.iter
+ (fun x ->
+ add_queue
+ (fun () ->
+ try
+ already_there x;
+ add emitter new_kf b.b_name x
+ with M.Found e ->
+ (* We keep x at its right place inside b. *)
+ remove e new_kf x;
+ add e new_kf b.b_name x))
+ (List.rev elts);
in
- let a =
- fold_elt
- { Fold.apply = Annotations.fold_allocates }
- Cil.visitCilAllocation
+ let register_annots b' f =
+ add_queue
+ (fun () -> ignore (Annotations.behaviors ~populate:false new_kf));
+ remove_and_add
+ (fun b -> b.b_requires)
+ Annotations.remove_requires
+ (fun e kf behavior r -> Annotations.add_requires e kf ~behavior [r])
+ Annotations.fold_requires
+ old_requires b';
+ remove_and_add
+ (fun b -> b.b_assumes)
+ Annotations.remove_assumes
+ (fun e kf behavior r -> Annotations.add_assumes e kf ~behavior [r])
+ Annotations.fold_assumes
+ old_assumes b';
+ remove_and_add
+ (fun b -> b.b_post_cond)
+ Annotations.remove_ensures
+ (fun e kf behavior r -> Annotations.add_ensures e kf ~behavior [r])
+ Annotations.fold_ensures
+ old_ensures b';
+ remove_and_add
+ (fun b -> match b.b_assigns with WritesAny -> [] | a -> [a])
+ Annotations.remove_assigns
+ (fun e kf behavior a ->
+ match a with
+ | WritesAny -> ()
+ | Writes _ ->
+ Annotations.add_assigns ~keep_empty:false e kf ~behavior a)
+ Annotations.fold_assigns
+ old_assigns b';
+ remove_and_add
+ (fun b -> match b.b_allocation with FreeAllocAny -> [] | a -> [a])
Annotations.remove_allocates
(fun e kf behavior a ->
Annotations.add_allocates ~keep_empty:false e kf ~behavior a)
- concat_allocation
- FreeAllocAny
- in
- b'.b_allocation <- a;
- let ext =
- fold_elt
- { Fold.apply = Annotations.fold_extended }
- Cil.visitCilExtended
+ Annotations.fold_allocates
+ old_allocates b';
+ remove_and_add
+ (fun b -> b.b_extended)
Annotations.remove_extended
(fun e kf behavior ex -> Annotations.add_extended e kf ~behavior ex)
- (fun x y -> x::y)
- []
+ Annotations.fold_extended
+ old_extended b';
+ f b'
in
- b'.b_extended <- ext;
- f b'
- in
- let remove_and_add get remove add fold old b =
- let emitter = match e with None -> Emitter.end_user | Some e -> e in
- let elts = get b in
- List.iter
- (fun (e,x) ->
- if not (List.memq x elts) then
- add_queue (fun () -> remove e new_kf x))
- old;
- let module M = struct exception Found of Emitter.t end in
- let already_there x =
- fold (fun e y () -> if x == y then raise (M.Found e)) new_kf b.b_name ()
- in
- List.iter
- (fun x ->
- add_queue
- (fun () ->
- try
- already_there x;
- add emitter new_kf b.b_name x
- with M.Found e ->
- (* We keep x at its right place inside b. *)
- remove e new_kf x;
- add e new_kf b.b_name x))
- (List.rev elts);
- in
- let register_annots b' f =
- add_queue
- (fun () -> ignore (Annotations.behaviors ~populate:false new_kf));
- remove_and_add
- (fun b -> b.b_requires)
- Annotations.remove_requires
- (fun e kf behavior r -> Annotations.add_requires e kf ~behavior [r])
- Annotations.fold_requires
- old_requires b';
- remove_and_add
- (fun b -> b.b_assumes)
- Annotations.remove_assumes
- (fun e kf behavior r -> Annotations.add_assumes e kf ~behavior [r])
- Annotations.fold_assumes
- old_assumes b';
- remove_and_add
- (fun b -> b.b_post_cond)
- Annotations.remove_ensures
- (fun e kf behavior r -> Annotations.add_ensures e kf ~behavior [r])
- Annotations.fold_ensures
- old_ensures b';
- remove_and_add
- (fun b -> match b.b_assigns with WritesAny -> [] | a -> [a])
- Annotations.remove_assigns
- (fun e kf behavior a ->
- match a with
- | WritesAny -> ()
- | Writes _ ->
- Annotations.add_assigns ~keep_empty:false e kf ~behavior a)
- Annotations.fold_assigns
- old_assigns b';
- remove_and_add
- (fun b -> match b.b_allocation with FreeAllocAny -> [] | a -> [a])
- Annotations.remove_allocates
- (fun e kf behavior a ->
- Annotations.add_allocates ~keep_empty:false e kf ~behavior a)
- Annotations.fold_allocates
- old_allocates b';
- remove_and_add
- (fun b -> b.b_extended)
- Annotations.remove_extended
- (fun e kf behavior ex -> Annotations.add_extended e kf ~behavior ex)
- Annotations.fold_extended
- old_extended b';
- f b'
- in
- match res with
+ match res with
| SkipChildren -> b
| JustCopy -> visit_clauses self#plain_copy_visitor Extlib.id
| JustCopyPost f -> visit_clauses self#plain_copy_visitor f
| ChangeTo b -> register_annots b Extlib.id
| ChangeToPost (b,f) -> register_annots b f
| ChangeDoChildrenPost (b,f) ->
- register_annots (Cil.childrenBehavior (self:>Cil.cilVisitor) b) f
+ register_annots (Cil.childrenBehavior (self:>Cil.cilVisitor) b) f
| DoChildren -> visit_clauses self Extlib.id
| DoChildrenPost f -> visit_clauses self f
- method private vfunspec_annot () =
- let kf = Extlib.the self#current_kf in
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- let old_behaviors =
- Annotations.fold_behaviors (fun e b acc -> (e,b)::acc) kf []
- in
- let old_complete =
- Annotations.fold_complete (fun e c acc -> (e,c)::acc) kf []
- in
- let old_disjoint =
- Annotations.fold_disjoint (fun e d acc -> (e,d)::acc) kf []
- in
- let old_terminates =
- Annotations.fold_terminates (fun e t _ -> Some (e,t)) kf None
- in
- let old_decreases =
- Annotations.fold_decreases (fun e d _ -> Some (e,d)) kf None
- in
- let spec =
- { spec_behavior = snd (List.split old_behaviors);
- spec_complete_behaviors = snd (List.split old_complete);
- spec_disjoint_behaviors = snd (List.split old_disjoint);
- spec_terminates =
- (Extlib.opt_map snd) old_terminates;
- spec_variant =
- (Extlib.opt_map snd) old_decreases
- }
- in
- let res = self#vspec spec in
- let do_children () =
- let new_behaviors =
- List.rev_map
- (fun (e,b) ->
- let b' = self#vbehavior_annot ~e b in
- if b != b' || kf != new_kf then begin
- Queue.add
- (fun () ->
- Annotations.add_behaviors
- ~register_children:false e new_kf [b'])
- self#get_filling_actions;
- end;
- b')
- old_behaviors
+ method private vfunspec_annot () =
+ let kf = Extlib.the self#current_kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ let old_behaviors =
+ Annotations.fold_behaviors (fun e b acc -> (e,b)::acc) kf []
in
- let new_terminates =
- Extlib.opt_map
- (fun (e,t) ->
- let t' = Cil.visitCilIdPredicate (self:>Cil.cilVisitor) t in
- if t != t' || kf != new_kf then
- Queue.add (fun () ->
- Annotations.remove_terminates e new_kf;
- Annotations.add_terminates e new_kf t')
- self#get_filling_actions
- ;
- t')
- old_terminates
+ let old_complete =
+ Annotations.fold_complete (fun e c acc -> (e,c)::acc) kf []
in
- let new_decreases =
- Extlib.opt_map
- (fun (e,(d,s as acc)) ->
- let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
- if d != d' || kf != new_kf then begin
- let res = (d',s) in
- Queue.add
- (fun () ->
- Annotations.remove_decreases e new_kf;
- Annotations.add_decreases e new_kf res;
- )
- self#get_filling_actions;
- res
- end else acc
- )
- old_decreases
+ let old_disjoint =
+ Annotations.fold_disjoint (fun e d acc -> (e,d)::acc) kf []
in
- if kf != new_kf then begin
- List.iter
- (fun (e,c) ->
- Queue.add (fun () -> Annotations.add_complete e new_kf c)
- self#get_filling_actions)
- (List.rev old_complete);
- List.iter
- (fun (e,d) ->
- Queue.add (fun () -> Annotations.add_disjoint e new_kf d)
- self#get_filling_actions)
- (List.rev old_disjoint)
- end;
- { spec with
- spec_behavior = new_behaviors;
- spec_terminates = new_terminates;
- spec_variant = new_decreases }
- in
- let change_do_children spec =
- let new_behaviors =
- Cil.mapNoCopy self#vbehavior_annot spec.spec_behavior
+ let old_terminates =
+ Annotations.fold_terminates (fun e t _ -> Some (e,t)) kf None
in
- let new_terminates =
- Cil.optMapNoCopy (Cil.visitCilIdPredicate (self:>Cil.cilVisitor))
- spec.spec_terminates
+ let old_decreases =
+ Annotations.fold_decreases (fun e d _ -> Some (e,d)) kf None
in
- let new_decreases =
- Cil.optMapNoCopy
- (fun (d,s as acc) ->
- let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
- if d != d' then (d',s) else acc)
- spec.spec_variant
+ let spec =
+ { spec_behavior = snd (List.split old_behaviors);
+ spec_complete_behaviors = snd (List.split old_complete);
+ spec_disjoint_behaviors = snd (List.split old_disjoint);
+ spec_terminates =
+ (Extlib.opt_map snd) old_terminates;
+ spec_variant =
+ (Extlib.opt_map snd) old_decreases
+ }
in
- { spec with
- spec_behavior = new_behaviors;
- spec_terminates = new_terminates;
- spec_variant = new_decreases }
- in
- let register_new_components new_spec =
- let add_spec_components () =
- let populate = false in
- let new_behaviors = Annotations.behaviors ~populate new_kf in
+ let res = self#vspec spec in
+ let do_children () =
+ let new_behaviors =
+ List.rev_map
+ (fun (e,b) ->
+ let b' = self#vbehavior_annot ~e b in
+ if b != b' || kf != new_kf then begin
+ Queue.add
+ (fun () ->
+ Annotations.add_behaviors
+ ~register_children:false e new_kf [b'])
+ self#get_filling_actions;
+ end;
+ b')
+ old_behaviors
+ in
+ let new_terminates =
+ Extlib.opt_map
+ (fun (e,t) ->
+ let t' = Cil.visitCilIdPredicate (self:>Cil.cilVisitor) t in
+ if t != t' || kf != new_kf then
+ Queue.add (fun () ->
+ Annotations.remove_terminates e new_kf;
+ Annotations.add_terminates e new_kf t')
+ self#get_filling_actions
+ ;
+ t')
+ old_terminates
+ in
+ let new_decreases =
+ Extlib.opt_map
+ (fun (e,(d,s as acc)) ->
+ let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
+ if d != d' || kf != new_kf then begin
+ let res = (d',s) in
+ Queue.add
+ (fun () ->
+ Annotations.remove_decreases e new_kf;
+ Annotations.add_decreases e new_kf res;
+ )
+ self#get_filling_actions;
+ res
+ end else acc
+ )
+ old_decreases
+ in
+ if kf != new_kf then begin
+ List.iter
+ (fun (e,c) ->
+ Queue.add (fun () -> Annotations.add_complete e new_kf c)
+ self#get_filling_actions)
+ (List.rev old_complete);
+ List.iter
+ (fun (e,d) ->
+ Queue.add (fun () -> Annotations.add_disjoint e new_kf d)
+ self#get_filling_actions)
+ (List.rev old_disjoint)
+ end;
+ { spec with
+ spec_behavior = new_behaviors;
+ spec_terminates = new_terminates;
+ spec_variant = new_decreases }
+ in
+ let change_do_children spec =
+ let new_behaviors =
+ Cil.mapNoCopy self#vbehavior_annot spec.spec_behavior
+ in
+ let new_terminates =
+ Cil.optMapNoCopy (Cil.visitCilIdPredicate (self:>Cil.cilVisitor))
+ spec.spec_terminates
+ in
+ let new_decreases =
+ Cil.optMapNoCopy
+ (fun (d,s as acc) ->
+ let d' = Cil.visitCilTerm (self:>Cil.cilVisitor) d in
+ if d != d' then (d',s) else acc)
+ spec.spec_variant
+ in
+ { spec with
+ spec_behavior = new_behaviors;
+ spec_terminates = new_terminates;
+ spec_variant = new_decreases }
+ in
+ let register_new_components new_spec =
+ let add_spec_components () =
+ let populate = false in
+ let new_behaviors = Annotations.behaviors ~populate new_kf in
+ List.iter
+ (fun b ->
+ if
+ (List.for_all
+ (fun x -> x.b_name <> b.b_name || Cil.is_empty_behavior x)
+ new_behaviors)
+ then begin
+ Annotations.add_behaviors ~register_children:false
+ Emitter.end_user new_kf [b]
+ end)
+ new_spec.spec_behavior;
+ let new_complete = Annotations.complete ~populate new_kf in
+ List.iter
+ (fun c ->
+ if not (List.memq c new_complete) then begin
+ Annotations.add_complete Emitter.end_user new_kf c
+ end)
+ new_spec.spec_complete_behaviors;
+ let new_disjoint = Annotations.disjoint ~populate new_kf in
+ List.iter
+ (fun d ->
+ if not (List.memq d new_disjoint) then
+ Annotations.add_disjoint Emitter.end_user new_kf d)
+ new_spec.spec_disjoint_behaviors;
+ let new_terminates = Annotations.terminates ~populate new_kf in
+ (match new_terminates, new_spec.spec_terminates with
+ | None, None -> ()
+ | Some _, None -> ()
+ | None, Some p ->
+ Annotations.add_terminates Emitter.end_user new_kf p
+ | Some p1, Some p2 when p1 == p2 -> ()
+ | Some p1, Some p2 ->
+ Kernel.fatal
+ "Visit of spec of function %a gives \
+ inconsistent terminates clauses@\n\
+ Registered @[%a@]@\nReturned @[%a@]"
+ Kernel_function.pretty new_kf
+ Printer.pp_identified_predicate p1
+ Printer.pp_identified_predicate p2);
+ let new_decreases = Annotations.decreases ~populate new_kf in
+ (match new_decreases, new_spec.spec_variant with
+ | None, None -> ()
+ | Some _, None -> ()
+ | None, Some p ->
+ Annotations.add_decreases Emitter.end_user new_kf p
+ | Some p1, Some p2 when p1 == p2 -> ()
+ | Some p1, Some p2 ->
+ Kernel.fatal
+ "Visit of spec of function %a gives \
+ inconsistent variant clauses@\n\
+ Registered %d@\n%a@\nReturned %d@\n%a"
+ Kernel_function.pretty new_kf
+ (Obj.magic p1)
+ Printer.pp_decreases p1
+ (Obj.magic p2)
+ Printer.pp_decreases p2)
+ in
List.iter
- (fun b ->
- if
- (List.for_all
- (fun x -> x.b_name <> b.b_name || Cil.is_empty_behavior x)
- new_behaviors)
- then begin
- Annotations.add_behaviors ~register_children:false
- Emitter.end_user new_kf [b]
- end)
- new_spec.spec_behavior;
- let new_complete = Annotations.complete ~populate new_kf in
+ (fun (e,c) ->
+ if not (List.memq c new_spec.spec_complete_behaviors) then
+ Queue.add
+ (fun () -> Annotations.remove_complete e new_kf c)
+ self#get_filling_actions)
+ old_complete;
List.iter
- (fun c ->
- if not (List.memq c new_complete) then begin
- Annotations.add_complete Emitter.end_user new_kf c
- end)
- new_spec.spec_complete_behaviors;
- let new_disjoint = Annotations.disjoint ~populate new_kf in
+ (fun (e,d) ->
+ if not (List.memq d new_spec.spec_disjoint_behaviors) then
+ Queue.add
+ (fun () -> Annotations.remove_disjoint e new_kf d)
+ self#get_filling_actions)
+ old_disjoint;
List.iter
- (fun d ->
- if not (List.memq d new_disjoint) then
- Annotations.add_disjoint Emitter.end_user new_kf d)
- new_spec.spec_disjoint_behaviors;
- let new_terminates = Annotations.terminates ~populate new_kf in
- (match new_terminates, new_spec.spec_terminates with
- | None, None -> ()
- | Some _, None -> ()
- | None, Some p ->
- Annotations.add_terminates Emitter.end_user new_kf p
- | Some p1, Some p2 when p1 == p2 -> ()
- | Some p1, Some p2 ->
- Kernel.fatal
- "Visit of spec of function %a gives \
- inconsistent terminates clauses@\n\
- Registered @[%a@]@\nReturned @[%a@]"
- Kernel_function.pretty new_kf
- Printer.pp_identified_predicate p1
- Printer.pp_identified_predicate p2);
- let new_decreases = Annotations.decreases ~populate new_kf in
- (match new_decreases, new_spec.spec_variant with
- | None, None -> ()
- | Some _, None -> ()
- | None, Some p ->
- Annotations.add_decreases Emitter.end_user new_kf p
- | Some p1, Some p2 when p1 == p2 -> ()
- | Some p1, Some p2 ->
- Kernel.fatal
- "Visit of spec of function %a gives \
- inconsistent variant clauses@\n\
- Registered %d@\n%a@\nReturned %d@\n%a"
- Kernel_function.pretty new_kf
- (Obj.magic p1)
- Printer.pp_decreases p1
- (Obj.magic p2)
- Printer.pp_decreases p2)
+ (fun (e,b) ->
+ if not (List.memq b new_spec.spec_behavior) then begin
+ Queue.add
+ (fun () ->
+ if
+ List.exists (fun x -> x.b_name = b.b_name)
+ new_spec.spec_behavior
+ then Annotations.remove_behavior_components e new_kf b
+ else Annotations.remove_behavior e new_kf b)
+ self#get_filling_actions
+ end
+ )
+ old_behaviors;
+ Extlib.may
+ (fun (e,t) ->
+ if not (Extlib.may_map
+ ~dft:false (fun t' -> t == t') new_spec.spec_terminates)
+ then
+ Queue.add
+ (fun () -> Annotations.remove_terminates e new_kf)
+ self#get_filling_actions)
+ old_terminates;
+ Extlib.may
+ (fun (e,d) ->
+ if not (Extlib.may_map
+ ~dft:false (fun d' -> d == d') new_spec.spec_variant)
+ then
+ Queue.add
+ (fun () -> Annotations.remove_decreases e new_kf)
+ self#get_filling_actions)
+ old_decreases;
+ Queue.add add_spec_components self#get_filling_actions;
in
- List.iter
- (fun (e,c) ->
- if not (List.memq c new_spec.spec_complete_behaviors) then
- Queue.add
- (fun () -> Annotations.remove_complete e new_kf c)
- self#get_filling_actions)
- old_complete;
- List.iter
- (fun (e,d) ->
- if not (List.memq d new_spec.spec_disjoint_behaviors) then
- Queue.add
- (fun () -> Annotations.remove_disjoint e new_kf d)
- self#get_filling_actions)
- old_disjoint;
- List.iter
- (fun (e,b) ->
- if not (List.memq b new_spec.spec_behavior) then begin
- Queue.add
- (fun () ->
- if
- List.exists (fun x -> x.b_name = b.b_name)
- new_spec.spec_behavior
- then Annotations.remove_behavior_components e new_kf b
- else Annotations.remove_behavior e new_kf b)
- self#get_filling_actions
- end
- )
- old_behaviors;
- Extlib.may
- (fun (e,t) ->
- if not (Extlib.may_map
- ~dft:false (fun t' -> t == t') new_spec.spec_terminates)
- then
- Queue.add
- (fun () -> Annotations.remove_terminates e new_kf)
- self#get_filling_actions)
- old_terminates;
- Extlib.may
- (fun (e,d) ->
- if not (Extlib.may_map
- ~dft:false (fun d' -> d == d') new_spec.spec_variant)
- then
- Queue.add
- (fun () -> Annotations.remove_decreases e new_kf)
- self#get_filling_actions)
- old_decreases;
- Queue.add add_spec_components self#get_filling_actions;
- in
- match res with
+ match res with
| SkipChildren -> register_new_components spec
| ChangeTo spec -> register_new_components spec
- | ChangeToPost (spec,f) ->
- register_new_components spec; ignore (f spec)
+ | ChangeToPost (spec,f) ->
+ register_new_components spec; ignore (f spec)
| JustCopy ->
- register_new_components
- (Cil.visitCilFunspec self#plain_copy_visitor spec)
+ register_new_components
+ (Cil.visitCilFunspec self#plain_copy_visitor spec)
| JustCopyPost f ->
- (register_new_components
- (Cil.visitCilFunspec self#plain_copy_visitor spec));
- ignore (f spec)
+ (register_new_components
+ (Cil.visitCilFunspec self#plain_copy_visitor spec));
+ ignore (f spec)
| DoChildren -> ignore (do_children ())
| DoChildrenPost f -> ignore (f (do_children ()))
| ChangeDoChildrenPost(spec, f) ->
- let res = change_do_children spec in
- register_new_components res;
- ignore (f res)
-
- method! vglob g =
- let fundec, has_kf = match g with
- | GFunDecl(_,v,_) ->
- let ov = Visitor_behavior.Get_orig.varinfo self#behavior v in
- let kf = try Globals.Functions.get ov with Not_found ->
- Kernel.fatal "No kernel function for %s(%d)" v.vname v.vid
- in
- (* Just make a copy of current kernel function in case it is needed *)
- let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
- if Visitor_behavior.is_copy self#behavior then
- new_kf.spec <- Cil.empty_funspec ();
- self#set_current_kf kf;
- None, true
- | GFun(f,_) ->
- let v = Visitor_behavior.Get_orig.varinfo self#behavior f.svar in
- let kf =
- try Globals.Functions.get v
- with Not_found ->
- Kernel.fatal "Visitor does not find function %s in %a"
- v.vname
- Project.pretty (Project.current ())
- in
- let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
- if Visitor_behavior.is_copy self#behavior then
- new_kf.spec <- Cil.empty_funspec ();
- self#set_current_kf kf;
- Some f, true
- | _ -> None, false
- in
- let res = self#vglob_aux g in
- let make_funspec () = match g with
- | GFunDecl _ | GFun _ when Ast.is_def_or_last_decl g ->
+ let res = change_do_children spec in
+ register_new_components res;
+ ignore (f res)
+
+ method! vglob g =
+ let fundec, has_kf = match g with
+ | GFunDecl(_,v,_) ->
+ let ov = Visitor_behavior.Get_orig.varinfo self#behavior v in
+ let kf = try Globals.Functions.get ov with Not_found ->
+ Kernel.fatal "No kernel function for %s(%d)" v.vname v.vid
+ in
+ (* Just make a copy of current kernel function in case it is needed *)
+ let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
+ if Visitor_behavior.is_copy self#behavior then
+ new_kf.spec <- Cil.empty_funspec ();
+ self#set_current_kf kf;
+ None, true
+ | GFun(f,_) ->
+ let v = Visitor_behavior.Get_orig.varinfo self#behavior f.svar in
+ let kf =
+ try Globals.Functions.get v
+ with Not_found ->
+ Kernel.fatal "Visitor does not find function %s in %a"
+ v.vname
+ Project.pretty (Project.current ())
+ in
+ let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
+ if Visitor_behavior.is_copy self#behavior then
+ new_kf.spec <- Cil.empty_funspec ();
+ self#set_current_kf kf;
+ Some f, true
+ | _ -> None, false
+ in
+ let res = self#vglob_aux g in
+ let make_funspec () = match g with
+ | GFunDecl _ | GFun _ when Ast.is_def_or_last_decl g ->
self#vfunspec_annot ();
- | _ -> ()
- in
- (* NB: we'll loose track of the emitter of an annotation.
- Anyway, this is only used for SkipChildren and JustCopy/JustCopyPost
- (and for a copy visitor)
- If user sticks to DoChildren, s/he'll still have the proper
- correspondence between annotations and emitters.
- *)
- let get_spec () = match g with
- | GFun _ | GFunDecl _ when Ast.is_def_or_last_decl g ->
- let spec =
- Annotations.funspec ~populate:false (Extlib.the self#current_kf)
- in
- Some (Cil.visitCilFunspec self#plain_copy_visitor spec)
- | _ -> None
- in
- let change_glob ng spec =
- let cond = Visitor_behavior.is_copy self#behavior in
- match ng with
+ | _ -> ()
+ in
+ (* NB: we'll loose track of the emitter of an annotation.
+ Anyway, this is only used for SkipChildren and JustCopy/JustCopyPost
+ (and for a copy visitor)
+ If user sticks to DoChildren, s/he'll still have the proper
+ correspondence between annotations and emitters.
+ *)
+ let get_spec () = match g with
+ | GFun _ | GFunDecl _ when Ast.is_def_or_last_decl g ->
+ let spec =
+ Annotations.funspec ~populate:false (Extlib.the self#current_kf)
+ in
+ Some (Cil.visitCilFunspec self#plain_copy_visitor spec)
+ | _ -> None
+ in
+ let change_glob ng spec =
+ let cond = Visitor_behavior.is_copy self#behavior in
+ match ng with
| GVar(vi,init,_) ->
- if cond then
- Queue.add
- (fun () ->
- try
- Globals.Vars.add vi init
- with Globals.Vars.AlreadyExists (vi,_) ->
- Kernel.fatal
- "Visitor is trying to insert global variable %a that \
- already exists in current project"
- Cil_datatype.Varinfo.pretty vi)
- self#get_filling_actions
+ if cond then
+ Queue.add
+ (fun () ->
+ try
+ Globals.Vars.add vi init
+ with Globals.Vars.AlreadyExists (vi,_) ->
+ Kernel.fatal
+ "Visitor is trying to insert global variable %a that \
+ already exists in current project"
+ Cil_datatype.Varinfo.pretty vi)
+ self#get_filling_actions
| GFunDecl(_,v,l) ->
- (match self#current_kf with
- | Some kf ->
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
- if cond then begin
- Queue.add
- (fun () ->
- if Cil.hasAttribute "FC_BUILTIN" v.vattr then
- Cil.Frama_c_builtins.add v.vname v;
- if Cil_datatype.Varinfo.equal v
- (Kernel_function.get_vi new_kf)
- then begin
- let dft =
- Annotations.funspec ~populate:false new_kf
- in
- let dft =
- { dft with spec_behavior = dft.spec_behavior }
- in
- let spec = Extlib.opt_conv dft spec in
- Globals.Functions.register new_kf;
- Globals.Functions.replace_by_declaration spec v l;
+ (match self#current_kf with
+ | Some kf ->
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ if cond then begin
+ Queue.add
+ (fun () ->
+ if Cil.hasAttribute "FC_BUILTIN" v.vattr then
+ Cil_builtins.Frama_c_builtins.add v.vname v;
+ if Cil_datatype.Varinfo.equal v
+ (Kernel_function.get_vi new_kf)
+ then begin
+ let dft =
+ Annotations.funspec ~populate:false new_kf
+ in
+ let dft =
+ { dft with spec_behavior = dft.spec_behavior }
+ in
+ let spec = Extlib.opt_conv dft spec in
+ Globals.Functions.register new_kf;
+ Globals.Functions.replace_by_declaration spec v l;
(* Format.printf "registered spec:@\n%a@." Printer.pp_funspec
(Annotations.funspec ~populate:false new_kf) *)
- end else begin
- Globals.Functions.replace_by_declaration
- (Cil.empty_funspec()) v l
- end)
- self#get_filling_actions;
- if
- Cil_datatype.Varinfo.equal v
- (Kernel_function.get_vi new_kf) && Extlib.has_some spec
- then
- Queue.add
- (fun () ->
- Annotations.register_funspec ~force:true new_kf)
- self#get_filling_actions;
- end
- | None -> ()
- (* User is responsible for registering the new function *)
- )
- | GVarDecl (({vstorage=Extern} as v),_) (* when not (isFunctionType
- v.vtype) *) ->
- if cond then
- Queue.add
- (fun () ->
- try
- Globals.Vars.add_decl v
- with Globals.Vars.AlreadyExists (vi,_) ->
- Kernel.fatal
- "Visitor is trying to insert global variable %a that \
- already exists in current project"
- Cil_datatype.Varinfo.pretty vi)
- self#get_filling_actions
- | GFun(f,l) ->
- if cond then begin
- match self#current_kf with
+ end else begin
+ Globals.Functions.replace_by_declaration
+ (Cil.empty_funspec()) v l
+ end)
+ self#get_filling_actions;
+ if
+ Cil_datatype.Varinfo.equal v
+ (Kernel_function.get_vi new_kf) && Extlib.has_some spec
+ then
+ Queue.add
+ (fun () ->
+ Annotations.register_funspec ~force:true new_kf)
+ self#get_filling_actions;
+ end
+ | None -> ()
+ (* User is responsible for registering the new function *)
+ )
+ | GVarDecl (({vstorage=Extern} as v),_) (* when not (isFunctionType
+ v.vtype) *) ->
+ if cond then
+ Queue.add
+ (fun () ->
+ try
+ Globals.Vars.add_decl v
+ with Globals.Vars.AlreadyExists (vi,_) ->
+ Kernel.fatal
+ "Visitor is trying to insert global variable %a that \
+ already exists in current project"
+ Cil_datatype.Varinfo.pretty vi)
+ self#get_filling_actions
+ | GFun(f,l) ->
+ if cond then begin
+ match self#current_kf with
| Some kf ->
- let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
+ Queue.add
+ (fun () ->
+ Kernel.debug ~dkey:Kernel.dkey_visitor
+ "@[Adding definition %s (vid: %d) for project %s@\n\
+ body: %a@\n@]@."
+ f.svar.vname f.svar.vid
+ (Project.get_name (Project.current()))
+ Printer.pp_block f.sbody;
+ if cond && Cil.hasAttribute "FC_BUILTIN" f.svar.vattr then
+ Cil_builtins.Frama_c_builtins.add f.svar.vname f.svar;
+ if Cil_datatype.Varinfo.equal f.svar
+ (Kernel_function.get_vi new_kf)
+ then begin
+ Globals.Functions.register new_kf;
+ let spec =
+ Extlib.opt_conv
+ (Annotations.funspec ~populate:false new_kf) spec
+ in
+ Globals.Functions.replace_by_definition spec f l
+ end else
+ Globals.Functions.replace_by_definition
+ (Cil.empty_funspec ()) f l
+ )
+ self#get_filling_actions;
+ if Cil_datatype.Varinfo.equal f.svar
+ (Kernel_function.get_vi new_kf)
+ && Extlib.has_some spec
+ then
Queue.add
- (fun () ->
- Kernel.debug ~dkey:Kernel.dkey_visitor
- "@[Adding definition %s (vid: %d) for project %s@\n\
- body: %a@\n@]@."
- f.svar.vname f.svar.vid
- (Project.get_name (Project.current()))
- Printer.pp_block f.sbody;
- if cond && Cil.hasAttribute "FC_BUILTIN" f.svar.vattr then
- Cil.Frama_c_builtins.add f.svar.vname f.svar;
- if Cil_datatype.Varinfo.equal f.svar
- (Kernel_function.get_vi new_kf)
- then begin
- Globals.Functions.register new_kf;
- let spec =
- Extlib.opt_conv
- (Annotations.funspec ~populate:false new_kf) spec
- in
- Globals.Functions.replace_by_definition spec f l
- end else
- Globals.Functions.replace_by_definition
- (Cil.empty_funspec ()) f l
- )
+ (fun () -> Annotations.register_funspec ~force:true new_kf)
self#get_filling_actions;
- if Cil_datatype.Varinfo.equal f.svar
- (Kernel_function.get_vi new_kf)
- && Extlib.has_some spec
- then
- Queue.add
- (fun () -> Annotations.register_funspec ~force:true new_kf)
- self#get_filling_actions;
| None -> () (* User has to register the new function *)
- end
- | GAnnot (na,_) when cond ->
- let e = match g with
- | GAnnot (a,_) -> Annotations.emitter_of_global a
- | _ -> Emitter.end_user
- in
- Queue.add
- (fun () ->
- try
- (* Annotations might have already been added by the user. *)
- ignore (Annotations.emitter_of_global na)
- with Not_found ->
- Annotations.unsafe_add_global e na;
- )
- self#get_filling_actions
- | _ -> ()
- in
- let post_action g =
- Extlib.may self#set_current_func fundec;
- let spec = get_spec () in
- List.iter (fun g -> change_glob g spec) g;
- if has_kf then self#reset_current_kf();
- Extlib.may (fun _ -> self#reset_current_func ()) fundec;
- g
- in
- let post_change_to g =
- List.iter (fun g -> change_glob g None) g;
- if has_kf then self#reset_current_kf();
- g
- in
- let post_do_children f g =
- Extlib.may self#set_current_func fundec;
- make_funspec ();
- let res = f g in
- (* Spec registration is already handled at the vfunspec level. *)
- List.iter (fun g -> change_glob g None) res;
- if has_kf then self#reset_current_kf();
- Extlib.may (fun _ -> self#reset_current_func ()) fundec;
- res
- in
- match res with
- | SkipChildren ->
+ end
+ | GAnnot (na,_) when cond ->
+ let e = match g with
+ | GAnnot (a,_) -> Annotations.emitter_of_global a
+ | _ -> Emitter.end_user
+ in
+ Queue.add
+ (fun () ->
+ try
+ (* Annotations might have already been added by the user. *)
+ ignore (Annotations.emitter_of_global na)
+ with Not_found ->
+ Annotations.unsafe_add_global e na;
+ )
+ self#get_filling_actions
+ | _ -> ()
+ in
+ let post_action g =
+ Extlib.may self#set_current_func fundec;
+ let spec = get_spec () in
+ List.iter (fun g -> change_glob g spec) g;
+ if has_kf then self#reset_current_kf();
+ Extlib.may (fun _ -> self#reset_current_func ()) fundec;
+ g
+ in
+ let post_change_to g =
+ List.iter (fun g -> change_glob g None) g;
+ if has_kf then self#reset_current_kf();
+ g
+ in
+ let post_do_children f g =
+ Extlib.may self#set_current_func fundec;
+ make_funspec ();
+ let res = f g in
+ (* Spec registration is already handled at the vfunspec level. *)
+ List.iter (fun g -> change_glob g None) res;
+ if has_kf then self#reset_current_kf();
+ Extlib.may (fun _ -> self#reset_current_func ()) fundec;
+ res
+ in
+ match res with
+ | SkipChildren ->
change_glob g None;
if has_kf then self#reset_current_kf();
res
- | JustCopy -> JustCopyPost post_action
- | JustCopyPost f -> JustCopyPost (post_action $ f)
- | DoChildren -> DoChildrenPost (post_do_children Extlib.id)
- | DoChildrenPost f -> DoChildrenPost (post_do_children f)
- | ChangeTo l -> ChangeToPost (l,post_change_to)
- | ChangeToPost (l,f) -> ChangeToPost (l, post_change_to $ f)
- | ChangeDoChildrenPost (l,f) -> ChangeDoChildrenPost (l, post_do_children f)
-end
+ | JustCopy -> JustCopyPost post_action
+ | JustCopyPost f -> JustCopyPost (post_action $ f)
+ | DoChildren -> DoChildrenPost (post_do_children Extlib.id)
+ | DoChildrenPost f -> DoChildrenPost (post_do_children f)
+ | ChangeTo l -> ChangeToPost (l,post_change_to)
+ | ChangeToPost (l,f) -> ChangeToPost (l, post_change_to $ f)
+ | ChangeDoChildrenPost (l,f) -> ChangeDoChildrenPost (l, post_do_children f)
+ end
class generic_frama_c_visitor bhv =
let current_kf = ref None in
diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli
index 068752c85685180f4f8f09aa766bb2be482bf738..fc7803bc7e876e5217cb2259938b2f4aa2eb3bfb 100644
--- a/src/kernel_services/visitors/visitor.mli
+++ b/src/kernel_services/visitors/visitor.mli
@@ -35,69 +35,69 @@ open Cil_types
{b A few hints on how to use correctly this visitor}
- when initializing a new project with it
- (see {!File.init_project_from_visitor}), use a visitor with copy behavior
+ (see {!File.init_project_from_visitor}), use a visitor with copy behavior
- [SkipChildren] and [ChangeTo] must be used with extreme care in a visitor
- with copy behavior, or some nodes may be shared between the original and
- the copy.
+ with copy behavior, or some nodes may be shared between the original and
+ the copy.
- Do not erase a statement during the visit, as there might be
- annotations attached to it. Change it to Skip instead, the
- [generic_frama_c_visitor] will know what to do.
+ annotations attached to it. Change it to Skip instead, the
+ [generic_frama_c_visitor] will know what to do.
- Be careful if you change the [vid] or [sid]: this must be done before
- anything has been attached to the corresponding variable or
- statement in the new project, which means
- - for statements, in [vstmt], for the current statement only
- - for variables, at their declaration point. *)
+ anything has been attached to the corresponding variable or
+ statement in the new project, which means
+ -- for statements, in [vstmt], for the current statement only
+ -- for variables, at their declaration point. *)
class type frama_c_visitor = object
inherit Cil.cilVisitor
method frama_c_plain_copy: frama_c_visitor
- (** same as plain_copy_visitor but for frama-c specific methods *)
+ (** same as plain_copy_visitor but for frama-c specific methods *)
method vstmt_aux: stmt -> stmt Cil.visitAction
- (** Replacement of vstmt.
- @plugin development guide*)
+ (** Replacement of vstmt.
+ @plugin development guide*)
method vglob_aux: global -> global list Cil.visitAction
- (** Replacement of vglob.
- @plugin development guide*)
+ (** Replacement of vglob.
+ @plugin development guide*)
method current_kf: kernel_function option
- (** link to the kernel function currently being visited.
- {b NB:} for copy visitors, the link is to the original kf (anyway,
- the new kf is created only after the visit is over).
- @plugin development guide *)
+ (** link to the kernel function currently being visited.
+ {b NB:} for copy visitors, the link is to the original kf (anyway,
+ the new kf is created only after the visit is over).
+ @plugin development guide *)
method set_current_kf: kernel_function -> unit
- (** Internal use only. *)
+ (** Internal use only. *)
method reset_current_kf: unit -> unit
- (** Internal use only. *)
+ (** Internal use only. *)
end
class frama_c_inplace: frama_c_visitor
- (** in-place visitor; always act in the current project.
- @plugin development guide *)
+(** in-place visitor; always act in the current project.
+ @plugin development guide *)
class frama_c_copy: Project.t -> frama_c_visitor
- (** Copying visitor. The [Project.t] argument specifies in which project the
- visitor creates the new values. (Technically, the method
- [fill_global_tables] is called inside this project.)
- See {!File.init_project_from_visitor} and [create_project_from_visitor]
- for possible uses. *)
+(** Copying visitor. The [Project.t] argument specifies in which project the
+ visitor creates the new values. (Technically, the method
+ [fill_global_tables] is called inside this project.)
+ See {!File.init_project_from_visitor} and [create_project_from_visitor]
+ for possible uses. *)
class frama_c_refresh: Project.t -> frama_c_visitor
- (** Similar to {!frama_c_copy}, but ids will be refreshed in the copy.
- @since Sodium-20150201
- *)
+(** Similar to {!frama_c_copy}, but ids will be refreshed in the copy.
+ @since Sodium-20150201
+*)
class generic_frama_c_visitor:
Visitor_behavior.t -> frama_c_visitor
- (** Generic class that abstracts over [frama_c_inplace] and [frama_c_copy].
- @plugin development guide *)
+(** Generic class that abstracts over [frama_c_inplace] and [frama_c_copy].
+ @plugin development guide *)
(** Visit a file. This will re-cons all globals TWICE (so that it is
tail-recursive). Use {!Cil.visitCilFileSameGlobals} if your visitor will
@@ -111,21 +111,21 @@ val visitFramacFile: frama_c_visitor -> file -> unit
(** A visitor for the whole file that does not change the globals (but maybe
changes things inside the globals). Use this function instead of
{!Visitor.visitFramacFile} whenever appropriate because it is more
- efficient for long files.
+ efficient for long files.
@plugin development guide *)
val visitFramacFileSameGlobals: frama_c_visitor -> file -> unit
(** Visit a global.
-{b Warning} Do not call this function during another visit using the
-same visitor, as it is not reentrant: the inner visit will leave the visitor
-in an inconsistent state for the outer visit.
+ {b Warning} Do not call this function during another visit using the
+ same visitor, as it is not reentrant: the inner visit will leave the visitor
+ in an inconsistent state for the outer visit.
*)
val visitFramacGlobal: frama_c_visitor -> global -> global list
(** Visit a kernel_function. More precisely, the entry point for the visit
will be the global corresponding to the last declaration/definition of
- the kf. The returned kf is the one that has the varinfo
+ the kf. The returned kf is the one that has the varinfo
associated to the varinfo of the original kf. If this is a new kf, it is
however the responsibility of the visitor to insert it in the AST at
the appropriate place.
@@ -165,7 +165,7 @@ val visitFramacType: frama_c_visitor -> typ -> typ
(** Visit a variable declaration *)
val visitFramacVarDecl: frama_c_visitor -> varinfo -> varinfo
-(** Visit a logic variable declaration
+(** Visit a logic variable declaration
@since Magnesium-20151001
*)
@@ -209,7 +209,7 @@ val visitFramacPredicates: frama_c_visitor -> identified_predicate list
(** visit identified_term.
@since Oxygen-20120901
- *)
+*)
val visitFramacIdTerm: frama_c_visitor -> identified_term -> identified_term
val visitFramacTerm: frama_c_visitor -> term -> term
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 20ea5cc48868ffe20489e1c40760f98aed23f723..76e2b68749813ef6c12eef46361b6ffc06559084 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -267,10 +267,17 @@ module Normalized = struct
if case_sensitive then String.compare s1 s2
else Extlib.compare_ignore_case s1 s2
- let pretty fmt p = Format.fprintf fmt "%s" (pretty p)
- let pp_abs fmt p = Format.fprintf fmt "%s" p
let unknown = normalize ""
let is_unknown fp = equal fp unknown
+ let special_stdout = normalize "-"
+ let is_special_stdout fp = equal fp special_stdout
+
+ let pretty fmt p =
+ if is_special_stdout p then
+ Format.fprintf fmt "<stdout>"
+ else
+ Format.fprintf fmt "%s" (pretty p)
+ let pp_abs fmt p = Format.fprintf fmt "%s" p
let is_file fp =
try
(Unix.stat (fp :> string)).Unix.st_kind = Unix.S_REG
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index e2958f5edda2dce7e56495f8640aab70854b9657..79a3d7fad11104bb79b5c4b5acc3909fcdb26e27 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -156,6 +156,11 @@ module Normalized: sig
(** @since 20.0-Calcium *)
val is_unknown: t -> bool
+ (** [is_special_stdout f] returns [true] iff [f] is '-' (a single dash),
+ which is a special notation for 'stdout'.
+ @since Frama-C+dev *)
+ val is_special_stdout: t -> bool
+
(** [is_file f] returns [true] iff [f] points to a regular file
(or a symbolic link pointing to a file).
Returns [false] if any errors happen when [stat]'ing the file.
diff --git a/src/plugins/e-acsl/doc/Makefile.common b/src/plugins/e-acsl/doc/Makefile.common
index 98ee1d0d781dd6339e17776ef4d08bca27c3c2e8..401488851dffe90acdef46c2121e429d115d41c2 100644
--- a/src/plugins/e-acsl/doc/Makefile.common
+++ b/src/plugins/e-acsl/doc/Makefile.common
@@ -1,7 +1,9 @@
# Common makefile for both refman and userman
VERSION_FILE=$(wildcard ../../../../../VERSION)
+CODENAME_FILE=$(wildcard ../../../../../VERSION_CODENAME)
EACSL_VERSION=$(shell cat $(VERSION_FILE))
+EACSL_CODENAME=$(shell cat $(CODENAME_FILE))
FC_VERSION=$(shell cat $(VERSION_FILE))
include $(EACSL_DIR)/doc/support/MakeLaTeXModern
@@ -10,9 +12,10 @@ include $(EACSL_DIR)/doc/support/MakeLaTeXModern
# Generic rules #
#################
-eacslversion.tex: Makefile $(VERSION_FILE)
+eacslversion.tex: Makefile $(VERSION_FILE) $(CODENAME_FILE)
rm -f $@
printf '\\newcommand{\\eacslpluginversion}{$(EACSL_VERSION)\\xspace}\n' > $@
+ printf '\\newcommand{\\eacslplugincodename}{$(EACSL_CODENAME)\\xspace}\n' >> $@
printf '\\newcommand{\\fcversion}{$(FC_VERSION)\\xspace}\n' >> $@
chmod a-w $@
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 43abe7595881b43a5c89f9168f0982a7b04e2dd2..44fd0956cf002e4351ef415c6d05236d4e67534e 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -1,6 +1,9 @@
\section{Changes}
-\subsection*{Version \version}
+% Next version
+%\subsection*{Version \version}
+
+\subsection*{Version 1.16}
\begin{itemize}
\item Update according to \acsl 1.16
\begin{itemize}
@@ -147,6 +150,9 @@ in \lstinline|\\at|}
{
\section{Changes in \eacsl Implementation}
+% Next version
+%\subsection*{Version \eacslplugincodename-\eacslpluginversion}
+
\subsection*{Version Titanium-22}
\begin{itemize}
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index a96a51aa43ba5125e0b05d9c209a6c45ff75909b..0d53e9d25dceefdf9e5f1d2e1f31a7288909e102 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -3,6 +3,9 @@
This chapter summarizes the changes in this documentation between each \eacsl
release. First we list changes of the last release.
+% Next version
+%\section*{E-ACSL \eacslpluginversion \eacslplugincodename}
+
\section*{E-ACSL 22.0 Titanium}
\begin{itemize}
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 3e3ce0bed39c979dc76141f7ab804793b492fd88..746d1444a183830b0a0579fa2694c3697e0d7f74 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -17,7 +17,7 @@
\includegraphics[height=14mm]{cealistlogo.jpg}
\end{flushleft}
\vfill
-\title{\eacsl Plug-in}{Release \eacslpluginversion
+\title{\eacsl Plug-in}{Release \eacslpluginversion (\eacslplugincodename)
\ifthenelse{\equal{\eacslpluginversion}{\fcversion}}{}{%
\\[1em] compatible with \framac \fcversion}}
\author{Julien Signoles, Basile Desloges and Kostyantyn Vorobyov}
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 7aafe514878534d25ce09b762a60bcf8db7776a0..11c177a27354c2c1881b88aece05394544979fff 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -28,7 +28,7 @@ open Cil_datatype
(* ************************************************************************** *)
let is_fc_or_compiler_builtin vi =
- Cil.is_builtin vi
+ Cil_builtins.is_builtin vi
||
(let prefix_length = 10 (* number of characters in "__builtin_" *) in
String.length vi.vname > prefix_length
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 69b3c42024f18b6584c06ef03d58eea1b1fa78fd..87ddec99e66d6debcd7956e8c86dae809d0f46b7 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -457,7 +457,7 @@ module State = struct
let is_unused = function
| GFun ({svar = vi},_) | GFunDecl (_, vi, _)
| GVar (vi, _, _) | GVarDecl (vi, _) ->
- Cil.is_unused_builtin vi
+ Cil_builtins.is_unused_builtin vi
| _ -> false
in
f, Extlib.filter_out is_unused all
diff --git a/src/plugins/gui/filetree.mli b/src/plugins/gui/filetree.mli
index 0cce6d677ca3f3f1f865c35ec23fbbd4eaa7e7be..bf353c76894432e5de4c568bd0bf29869aeb681b 100644
--- a/src/plugins/gui/filetree.mli
+++ b/src/plugins/gui/filetree.mli
@@ -25,70 +25,71 @@
type filetree_node =
| File of Datatype.Filepath.t * Cil_types.global list
| Global of Cil_types.global
-(** Caml type for the infos on a node of the tree. Not all globals appear
- in the filetree. Currently, the visible ones are:
- - functions definitions, or declarations if no definition exists
- - global variables
- - global annotations
- @since Nitrogen-20111001 *)
+ (** Caml type for the infos on a node of the tree. Not all globals appear
+ in the filetree. Currently, the visible ones are:
+ - functions definitions, or declarations if no definition exists
+ - global variables
+ - global annotations
+
+ @since Nitrogen-20111001 *)
class type t = object
method model : GTree.model
method flat_mode: bool
- (** Return [true] if the filetree currently displays all globals in
- flat mode (all children of the same node), [false] otherwise
- (children of the file they are declared in). If [true], the methods
- [set_file_attribute] and [get_files_globals] must not be used
+ (** Return [true] if the filetree currently displays all globals in
+ flat mode (all children of the same node), [false] otherwise
+ (children of the file they are declared in). If [true], the methods
+ [set_file_attribute] and [get_files_globals] must not be used
- @since Nitrogen-20111001 *)
+ @since Nitrogen-20111001 *)
method set_file_attribute:
?strikethrough:bool -> ?text:string -> Datatype.Filepath.t -> unit
- (** Manually set some attributes of the given filename. *)
+ (** Manually set some attributes of the given filename. *)
method set_global_attribute:
?strikethrough:bool -> ?text:string -> Cil_types.varinfo -> unit
- (** Manually set some attributes of the given variable. *)
+ (** Manually set some attributes of the given variable. *)
method add_global_filter:
text:string ->
key:string ->
(Cil_types.global -> bool) ->
(unit -> bool) * GMenu.check_menu_item
- (** [add_global_filter text key f] adds a filter for the visibility of
- the globals, according to [f]. If any of the filters registered
- through this method returns true, the global is not displayed in the
- filetree. [text] is used in the filetree menu, to label the entry
- permitting to activate or deactivate the filter. [key] is used to
- store the current state of the filter internally. The created
- menu is returned.
-
- @since Nitrogen-20111001
- @modify Oxygen-20120901 Signature change for the filter argument,
- return the menu.
- *)
+ (** [add_global_filter text key f] adds a filter for the visibility of
+ the globals, according to [f]. If any of the filters registered
+ through this method returns true, the global is not displayed in the
+ filetree. [text] is used in the filetree menu, to label the entry
+ permitting to activate or deactivate the filter. [key] is used to
+ store the current state of the filter internally. The created
+ menu is returned.
+
+ @since Nitrogen-20111001
+ @modify Oxygen-20120901 Signature change for the filter argument,
+ return the menu.
+ *)
method get_file_globals:
Datatype.Filepath.t -> (string * bool) list
- (** Return the names and the attributes (currently only the strikethrough
- property) of the globals in the file passed as argument *)
+ (** Return the names and the attributes (currently only the strikethrough
+ property) of the globals in the file passed as argument *)
method find_visible_global:
string -> Cil_types.global option
- (** [find_visible_global str] searches for the next occurrence of a visible
- global whose name contains [str], starting at the currently selected
- element. Returns the global found (if any).
+ (** [find_visible_global str] searches for the next occurrence of a visible
+ global whose name contains [str], starting at the currently selected
+ element. Returns the global found (if any).
- @since Magnesium-20151001 *)
+ @since Magnesium-20151001 *)
method add_select_function :
(was_activated:bool -> activating:bool -> filetree_node -> unit) -> unit
- (** Register a callback that is called whenever an element of the file tree
- is selected or unselected.
+ (** Register a callback that is called whenever an element of the file tree
+ is selected or unselected.
- @modify Nitrogen-20111001 Changed argument from a list
- of globals to [filetree_node] *)
+ @modify Nitrogen-20111001 Changed argument from a list
+ of globals to [filetree_node] *)
method append_text_column:
title:string ->
@@ -137,27 +138,27 @@ class type t = object
a [varinfo]. Returns a boolean to indicate success or failure. *)
method selected_globals : Cil_types.global list
- (** @since Carbon-20101201
- @return the list of selected globals in the treeview. *)
+ (** @since Carbon-20101201
+ @return the list of selected globals in the treeview. *)
method view : GTree.view
- (** The tree view associated in which the file tree is packed. *)
+ (** The tree view associated in which the file tree is packed. *)
method reset : unit -> unit
- (** Resynchronize the tree view with the current project state.
- This is called in particular by the generic reset extension of
- {!Design} *)
+ (** Resynchronize the tree view with the current project state.
+ This is called in particular by the generic reset extension of
+ {!Design} *)
method register_reset_extension : (t -> unit) -> unit
(** Register a function to be called whenever the reset method of the
filetree is called. *)
method refresh_columns : unit -> unit
- (** Refresh the state of all the non-source columns of the filetree,
- by hiding those that should be hidden, and displaying the
- others. Called by [reset]
+ (** Refresh the state of all the non-source columns of the filetree,
+ by hiding those that should be hidden, and displaying the
+ others. Called by [reset]
- @since Nitrogen-20111001 *)
+ @since Nitrogen-20111001 *)
end
val make : GTree.view -> t
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index e2f62844d00d39aac3e2c09cc96e44f7b8138d3e..df76889e7f2e7ba273a5b02f05933cd791d9e2af 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -688,7 +688,7 @@ let make_panel (main_ui:main_window_extension_points) =
(* Will the results for this kf be ultimately displayed *)
let display kf =
- not (Cil.is_unused_builtin (Kernel_function.get_vi kf)) &&
+ not (Cil_builtins.is_unused_builtin (Kernel_function.get_vi kf)) &&
not (onlyCurrent.get ()) ||
(let kfvi = Kernel_function.get_vi kf in
List.exists
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index f39592a07eb42ec3a47de75bc6ac63ee797cdebc..6bbea44d76f2e70d36867519f9277b9094d7acc6 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -34,7 +34,7 @@ let html_stag_functions =
let index = String.index t ' ' in
Format.sprintf "</%s>" (String.sub t 0 index)
with
- | Not_found -> Format.sprintf "</%s>" t
+ | Not_found -> Format.sprintf "</%s>" t
and print_open_stag _ = ()
and print_close_stag _ = ()
in
@@ -64,7 +64,7 @@ module OptionKf =
(** Defining base metrics and operations on those *)
module BasicMetrics = struct
-(** Record type to compute cyclomatic complexity *)
+ (** Record type to compute cyclomatic complexity *)
type t = {
cfile_name : Datatype.Filepath.t;
@@ -139,11 +139,11 @@ module BasicMetrics = struct
;;
let labels =
- [ "Sloc"; "Decision point"; "Global variables"; "If"; "Loop"; "Goto";
- "Assignment"; "Exit point"; "Function"; "Function call";
- "Pointer dereferencing";
- "Cyclomatic complexity";
- ]
+ [ "Sloc"; "Decision point"; "Global variables"; "If"; "Loop"; "Goto";
+ "Assignment"; "Exit point"; "Function"; "Function call";
+ "Pointer dereferencing";
+ "Cyclomatic complexity";
+ ]
;;
let str_values metrics =
@@ -162,12 +162,12 @@ module BasicMetrics = struct
let pp_func_or_none =
Pretty_utils.pp_opt ~none:"<none>" Kernel_function.pretty
-(* Pretty print metrics as text eg. in stdout *)
+ (* Pretty print metrics as text eg. in stdout *)
let pp_base_metrics fmt metrics =
let heading =
if metrics.cfile_name = Datatype.Filepath.dummy &&
metrics.cfunc = None then
- (* It is a global metrics *)
+ (* It is a global metrics *)
"Global metrics"
else
Format.asprintf "Stats for function <%a/%a>"
@@ -177,12 +177,12 @@ module BasicMetrics = struct
Format.fprintf fmt "@[<v 0>%a @ %a@]"
(mk_hdr 1) heading
((fun l1 ppf l2 ->
- List.iter2 (fun x y -> Format.fprintf ppf "%s = %s@ " x y)
- l1 l2) labels)
+ List.iter2 (fun x y -> Format.fprintf ppf "%s = %s@ " x y)
+ l1 l2) labels)
(str_values metrics)
;;
-(* Dummy utility functions for pretty printing simple types *)
+ (* Dummy utility functions for pretty printing simple types *)
let pp_int fmt n = Format.fprintf fmt "%d" n
;;
@@ -242,7 +242,7 @@ let get_suffix filename =
String.sub filename (succ last_dot_idx) (slen - last_dot_idx - 1)
else ""
with
- | Not_found -> raise No_suffix
+ | Not_found -> raise No_suffix
;;
type output_type =
@@ -254,16 +254,16 @@ type output_type =
let get_file_type filename =
try
match get_suffix filename with
- | "html" | "htm" -> Html
- | "txt" | "text" -> Text
- | "json" -> Json
- | s ->
- Metrics_parameters.abort
- "Unknown file extension %s. Cannot produce output.@." s
+ | "html" | "htm" -> Html
+ | "txt" | "text" -> Text
+ | "json" -> Json
+ | s ->
+ Metrics_parameters.abort
+ "Unknown file extension %s. Cannot produce output.@." s
with
- | No_suffix ->
- Metrics_parameters.abort
- "File %s has no suffix. Cannot produce output.@." filename
+ | No_suffix ->
+ Metrics_parameters.abort
+ "File %s has no suffix. Cannot produce output.@." filename
module VarinfoByName = struct
type t = Cil_types.varinfo
@@ -280,10 +280,10 @@ let pretty_set fmt s =
Format.fprintf fmt "@[";
VInfoMap.iter
(fun f n ->
- Format.fprintf fmt "%s %s(%d call%s);@ "
- f.Cil_types.vname
- (if f.vaddrof then "(address taken) " else "")
- n (if n > 1 then "s" else ""))
+ Format.fprintf fmt "%s %s(%d call%s);@ "
+ f.Cil_types.vname
+ (if f.vaddrof then "(address taken) " else "")
+ n (if n > 1 then "s" else ""))
s;
Format.fprintf fmt "@]"
@@ -318,8 +318,8 @@ let pretty_entry_points fmt fs =
let print fmt =
VInfoMap.iter
(fun fvinfo n ->
- if is_entry_point fvinfo n
- then Format.fprintf fmt "%s;@ " fvinfo.vname)
+ if is_entry_point fvinfo n
+ then Format.fprintf fmt "%s;@ " fvinfo.vname)
in
Format.fprintf fmt "@[<hov 1>%a@]" print fs;
;;
@@ -339,7 +339,7 @@ let json_of_entry_points m =
let file_of_vinfodef fvinfo =
let kf = Globals.Functions.get fvinfo in
let decl_loc1, _decl_loc2 =
- match kf.fundec with
+ match kf.fundec with
| Definition (_, loc) -> loc
| Declaration (_, _, _, loc) -> loc
in decl_loc1.Filepath.pos_path
@@ -353,12 +353,12 @@ let file_of_fundef (fun_dec: Cil_types.fundec) =
let extract_fundef_name sname =
match sname with
- | _spec, (the_name, _, _, _) -> the_name
+ | _spec, (the_name, _, _, _) -> the_name
;;
let kf_of_cabs_name sname =
match sname with
- | _spec, (the_name, _, _, _) -> Globals.Functions.find_by_name the_name
+ | _spec, (the_name, _, _, _) -> Globals.Functions.find_by_name the_name
let get_filename fdef =
match fdef with
@@ -370,12 +370,12 @@ let get_filename fdef =
let consider_function ~libc vinfo =
not (!Db.Value.mem_builtin vinfo.vname
|| Ast_info.is_frama_c_builtin vinfo.vname
- || Cil.is_unused_builtin vinfo
- ) && (libc || not (is_in_libc vinfo.vattr))
+ || Cil_builtins.is_unused_builtin vinfo
+ ) && (libc || not (is_in_libc vinfo.vattr))
let consider_variable ~libc vinfo =
not (Cil.hasAttribute "FRAMA_C_MODEL" vinfo.vattr) &&
- (libc || not (is_in_libc vinfo.vattr))
+ (libc || not (is_in_libc vinfo.vattr))
let float_to_string f =
let s = Format.sprintf "%F" f in
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index 1b209bbd078e665182942b0bba4e0c18d96e3e21..6e4b361b7bfa7c4b5d26e0234ff54b1973211aea 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -29,6 +29,7 @@ val html_stag_functions : Format.formatter_stag_functions;;
- level 1 headers are underlined by '='
- level 2 headers by '-'
- level 3 headers by '~'
+
This function is supposed to follow reStructuredText's conventions.
*)
val mk_hdr : int -> Format.formatter -> string -> unit;;
@@ -52,7 +53,7 @@ module BasicMetrics : sig
function, possibly more for a file.*)
cptrs: int ; (** Access to pointers *)
cdecision_points: int ; (** Decision points of the program: ifs,
- switch cases, exception handlers, ... *)
+ switch cases, exception handlers, ... *)
cglob_vars: int; (** Global variables *)
ccyclo: int; (** Cyclomatic complexity *)
}
@@ -164,7 +165,7 @@ val consider_variable: libc:bool -> Cil_types.varinfo -> bool
(** Convert float to string with the following convention:
- if the float is an integer (ie, it has no digits after the decimal point),
- print it as such;
+ print it as such;
- otherwise, print the first two digits after the decimal point.
*)
val float_to_string : float -> string ;;
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index adbe1215a838a78ebd76bbfc1f087e3aa716e9be..1659f351c48619b0c006120fa14ec4631c19bd99 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -57,7 +57,7 @@ class visitor = object
Cil.DoChildren
| GVarDecl (v, _) | GVar (v, _, _)
| GFun ({svar = v}, _) | GFunDecl (_, v, _)
- when Cil.is_unused_builtin v ->
+ when Cil_builtins.is_unused_builtin v ->
Cil.SkipChildren
| _ ->
Cil.DoChildren
@@ -101,8 +101,8 @@ class visitor = object
else begin
if Cil.isFunctionType vi.vtype then begin
if vi.vname <> "main"
- && not (Cil.is_builtin vi)
- && not (Cil.is_special_builtin vi.vname)
+ && not (Cil_builtins.is_builtin vi)
+ && not (Cil_builtins.is_special_builtin vi.vname)
&& not (Cil.hasAttribute "fc_stdlib" vi.vattr) then
vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname
end
diff --git a/src/plugins/report/scan.ml b/src/plugins/report/scan.ml
index b55fb12883f40017a80c29a53a0646379cffd49f..22a116f5a246a1f423a1d30870112e723e582094 100644
--- a/src/plugins/report/scan.ml
+++ b/src/plugins/report/scan.ml
@@ -147,7 +147,7 @@ let iter (inspector:inspector) =
Kernel_function.Map.iter
(fun kf ips ->
let vi = Kernel_function.get_vi kf in
- if not (Cil.is_unused_builtin vi) then
+ if not (Cil_builtins.is_unused_builtin vi) then
report (fun () -> inspector#function_section kf) inspector#property !ips)
!functions ;
inspector#finished ;
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 9ca090505b8adc0c4cfe86d339f3c8f3abdc63ec..511c5299a0e354b86bef51f466c5d02b060e0eef 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -314,7 +314,7 @@ let is_relevant ip =
| None -> true
| Some kf ->
not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
- || Cil.is_unused_builtin (Kernel_function.get_vi kf))
+ || Cil_builtins.is_unused_builtin (Kernel_function.get_vi kf))
let iter f = Property_status.iter (fun ip -> if is_relevant ip then f ip)
let add_update_hook f =
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 6138cf6f8591bf41d5e0b8f267463980879570b5..347fa439b5f714a833a7011884758de3870d6dcd 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -358,8 +358,8 @@ open Cil_types
let plural count = if count = 1 then "" else "s"
let consider_function vi =
- not (Cil.is_builtin vi
- || Cil.is_special_builtin vi.vname
+ not (Cil_builtins.is_builtin vi
+ || Cil_builtins.is_special_builtin vi.vname
|| Cil.hasAttribute "fc_stdlib" vi.vattr
|| Cil.hasAttribute "fc_stdlib_generated" vi.vattr)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 6647c539acf0696c7c8f7f84eda30496e9ffe98f..de29ab14d029903c2f43518d39f3820082cc6313 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -85,17 +85,17 @@ module V = struct
let is_imprecise v =
match v with
- | Top _ -> true
- | _ -> false
+ | Top _ -> true
+ | _ -> false
- let is_topint v = equal top_int v
+ let is_topint v = equal top_int v
let is_bottom v = equal bottom v
let is_isotropic v =
match v with
- | Top _ -> true
- | Map _ -> is_topint v || is_bottom v || is_zero v
+ | Top _ -> true
+ | Map _ -> is_topint v || is_bottom v || is_zero v
let contains_zero loc =
let offset_contains_zero base offset =
@@ -192,7 +192,7 @@ module V = struct
let o, ok = conv_offset o in
if o = NoOffset then
let o' = match Cil.unrollType typ_base with
- | TArray _ -> Index (Cil.(zero builtinLoc), NoOffset)
+ | TArray _ -> Index (Cil.(zero Cil_builtins.builtinLoc), NoOffset)
| TComp (ci, _, _) -> Field (List.hd ci.cfields, NoOffset)
| _ -> raise Bit_utils.NoMatchingOffset
in o', ok
@@ -271,17 +271,17 @@ module V = struct
let backward_rel_int_left op l r =
let open Abstract_interp.Comp in
match l with
- | Top _ -> l
- | Map m1 ->
- try
- let k,v2 = find_lonely_key r in
- let v1 = find_or_bottom k m1 in
- let v1' = Ival.backward_comp_int_left op v1 v2 in
- let r = add k v1' l in
- if (not (Base.equal k Base.null)) && (op = Ge || op = Gt)
- then diff_if_one r singleton_zero
- else r
- with Not_found -> l
+ | Top _ -> l
+ | Map m1 ->
+ try
+ let k,v2 = find_lonely_key r in
+ let v1 = find_or_bottom k m1 in
+ let v1' = Ival.backward_comp_int_left op v1 v2 in
+ let r = add k v1' l in
+ if (not (Base.equal k Base.null)) && (op = Ge || op = Gt)
+ then diff_if_one r singleton_zero
+ else r
+ with Not_found -> l
(* More aggressive reduction by relational pointer operators. This version
assumes that \pointer_comparable alarms have been emitted, and that
@@ -313,8 +313,8 @@ module V = struct
(* i1' and p1' are pointwise application of the comparison operator,
and will be in the result in all cases. *)
if debug then Kernel.result "%a %a %a %a %a -> %a %a"
- Ival.pretty il pretty pl pretty_comp op Ival.pretty ir pretty pr
- Ival.pretty il' pretty pl';
+ Ival.pretty il pretty pl pretty_comp op Ival.pretty ir pretty pr
+ Ival.pretty il' pretty pl';
match op, zl, zr with
| (Le | Lt), false, _ (* il + pl <~ (ir + ?0) + pr *)
| (Ge | Gt), _, false (* (il + ?0) + pl >~ ir + pr *) ->
@@ -375,10 +375,10 @@ module V = struct
|| (e2_zero && (op = Ge || op = Gt))
then True (* if e1/e2 is NULL, then e2/e1 is a pointer *)
else
- if (e2_zero && (op = Le || op = Lt))
- || (e1_zero && (op = Ge || op = Gt))
- then False
- else Unknown
+ if (e2_zero && (op = Le || op = Lt))
+ || (e1_zero && (op = Ge || op = Gt))
+ then False
+ else Unknown
end
end
with Not_found -> Comp.Unknown
@@ -393,9 +393,9 @@ module V = struct
let forward_comp_int ~signed op v1 v2 =
let open Abstract_interp.Comp in
match op with
- | Eq -> forward_eq_int v1 v2
- | Ne -> inv_truth (forward_eq_int v1 v2)
- | Le | Ge | Lt | Gt -> forward_rel_int ~signed op v1 v2
+ | Eq -> forward_eq_int v1 v2
+ | Ne -> inv_truth (forward_eq_int v1 v2)
+ | Le | Ge | Lt | Gt -> forward_rel_int ~signed op v1 v2
(** Casts and reinterpretation *)
@@ -428,9 +428,9 @@ module V = struct
(* ok_garbled indicates that we do _not_ create a (new) garbled mix *)
let pointer_part', ok_garbled =
if Int.ge size (Int.of_int (Bit_utils.sizeofpointer ())) ||
- is_bottom pointer_part || is_imprecise pointer_part
+ is_bottom pointer_part || is_imprecise pointer_part
then pointer_part, true
- else topify_arith_origin pointer_part, false
+ else topify_arith_origin pointer_part, false
in
if ok_garbled && integer_part' == integer_part then
v (* both pointer and integer part are unchanged *)
@@ -444,38 +444,38 @@ module V = struct
to_int Ival.reinterpret_as_int ~size ~signed v
let cast_float_to_int ~signed ~size v =
- try
- let v1 = project_ival v in
- let r = Ival.cast_float_to_int ~signed ~size v1 in
- inject_ival r
- with Not_based_on_null ->
- if is_bottom v
- then v
- else topify_arith_origin v
-
- let cast_float_to_int_inverse ~single_precision i =
- try
- let v1 = project_ival i in
- let r = Ival.cast_float_to_int_inverse ~single_precision v1 in
- Some (inject_ival r)
- with Not_based_on_null -> None
-
- let cast_int_to_float kind v =
- try
- let i = project_ival v in
- let r = Ival.cast_int_to_float kind i in
- inject_ival r
- with Not_based_on_null ->
- if is_bottom v
- then bottom
- else topify_arith_origin v
-
- let cast_int_to_float_inverse ~single_precision vf =
- try
- let ivf = project_ival vf in
- let i = Ival.cast_int_to_float_inverse ~single_precision ivf in
- Some (inject_ival i)
- with Not_based_on_null -> None
+ try
+ let v1 = project_ival v in
+ let r = Ival.cast_float_to_int ~signed ~size v1 in
+ inject_ival r
+ with Not_based_on_null ->
+ if is_bottom v
+ then v
+ else topify_arith_origin v
+
+ let cast_float_to_int_inverse ~single_precision i =
+ try
+ let v1 = project_ival i in
+ let r = Ival.cast_float_to_int_inverse ~single_precision v1 in
+ Some (inject_ival r)
+ with Not_based_on_null -> None
+
+ let cast_int_to_float kind v =
+ try
+ let i = project_ival v in
+ let r = Ival.cast_int_to_float kind i in
+ inject_ival r
+ with Not_based_on_null ->
+ if is_bottom v
+ then bottom
+ else topify_arith_origin v
+
+ let cast_int_to_float_inverse ~single_precision vf =
+ try
+ let ivf = project_ival vf in
+ let i = Ival.cast_int_to_float_inverse ~single_precision ivf in
+ Some (inject_ival i)
+ with Not_based_on_null -> None
(** Binary functions *)
@@ -485,13 +485,13 @@ module V = struct
let v2 = project_ival e2 in
inject_ival (f v1 v2)
with Not_based_on_null ->
- if is_bottom e1 || is_bottom e2
+ if is_bottom e1 || is_bottom e2
then bottom
else begin
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
- end
+ join
+ (topify_with_origin_kind topify e1)
+ (topify_with_origin_kind topify e2)
+ end
let arithmetic_function = import_function ~topify:Origin.K_Arith
@@ -520,23 +520,23 @@ module V = struct
try
Location_Bytes.shift (project_ival_bottom e2) e1
with Not_based_on_null ->
- try (* On the off chance that someone writes [i+(int)&p]... *)
- Location_Bytes.shift (project_ival_bottom e1) e2
- with Not_based_on_null ->
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ try (* On the off chance that someone writes [i+(int)&p]... *)
+ Location_Bytes.shift (project_ival_bottom e1) e2
+ with Not_based_on_null ->
+ join
+ (topify_with_origin_kind topify e1)
+ (topify_with_origin_kind topify e2)
end
with Not_found ->
- (* we end up here if the only way left to make this
- addition is to convert e2 to an integer *)
- try
- let right = Ival.scale_int_base factor (project_ival_bottom e2)
- in Location_Bytes.shift right e1
- with Not_based_on_null -> (* from [project_ival] *)
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ (* we end up here if the only way left to make this
+ addition is to convert e2 to an integer *)
+ try
+ let right = Ival.scale_int_base factor (project_ival_bottom e2)
+ in Location_Bytes.shift right e1
+ with Not_based_on_null -> (* from [project_ival] *)
+ join
+ (topify_with_origin_kind topify e1)
+ (topify_with_origin_kind topify e2)
(* Under-approximating variant of add_untyped. Takes two
under-approximation, and returns an under-approximation.*)
@@ -544,13 +544,13 @@ module V = struct
if Int_Base.equal factor (Int_Base.minus_one)
then
(* Note: we could do a "link" for each pair of matching bases in
- e1 and e2, so this is an underapproximation in the most
- common case. *)
+ e1 and e2, so this is an underapproximation in the most
+ common case. *)
try
- let b1, o1 = Location_Bytes.find_lonely_key e1 in
- let b2, o2 = Location_Bytes.find_lonely_key e2 in
- if Base.compare b1 b2 <> 0 then bottom
- else inject_ival (Ival.sub_int_under o1 o2)
+ let b1, o1 = Location_Bytes.find_lonely_key e1 in
+ let b2, o2 = Location_Bytes.find_lonely_key e2 in
+ if Base.compare b1 b2 <> 0 then bottom
+ else inject_ival (Ival.sub_int_under o1 o2)
with Not_found -> bottom
else if Int_Base.equal factor Int_Base.one
then
@@ -558,8 +558,8 @@ module V = struct
with Not_based_on_null -> bottom
else
try
- let right = Ival.scale_int_base factor (project_ival_bottom e2) in
- Location_Bytes.shift_under right e1
+ let right = Ival.scale_int_base factor (project_ival_bottom e2) in
+ Location_Bytes.shift_under right e1
with Not_based_on_null -> bottom
;;
@@ -648,14 +648,14 @@ module V = struct
let merge_distinct_bits ~topify ~conflate_bottom value acc =
if is_bottom acc || is_bottom value
then begin
- if conflate_bottom
- then
- bottom
- else
- join
- (topify_with_origin_kind topify acc)
- (topify_with_origin_kind topify value)
- end
+ if conflate_bottom
+ then
+ bottom
+ else
+ join
+ (topify_with_origin_kind topify acc)
+ (topify_with_origin_kind topify value)
+ end
else
add_untyped ~topify ~factor:Int_Base.one value acc
@@ -668,7 +668,7 @@ module V = struct
try
let i = project_ival v in
Ival.all_values ~size i
- with Not_based_on_null ->
+ with Not_based_on_null ->
false
let anisotropic_cast ~size v =
@@ -690,7 +690,7 @@ module V = struct
let add_untyped ~factor v1 v2 =
add_untyped ~topify:Origin.K_Arith ~factor v1 v2
-
+
end
module V_Or_Uninitialized = struct
@@ -706,10 +706,10 @@ module V_Or_Uninitialized = struct
let make ~initialized ~escaping v =
match initialized, escaping with
- | true, false -> C_init_noesc v
- | true, true -> C_init_esc v
- | false, false -> C_uninit_noesc v
- | false, true -> C_uninit_esc v
+ | true, false -> C_init_noesc v
+ | true, true -> C_init_esc v
+ | false, false -> C_uninit_noesc v
+ | false, true -> C_uninit_esc v
let mask_init = 2
let mask_noesc = 1
@@ -719,7 +719,7 @@ module V_Or_Uninitialized = struct
let is_initialized v = (get_flags v land mask_init) <> 0
let is_noesc v = (get_flags v land mask_noesc) <> 0
- let get_v = function
+ let get_v = function
| C_uninit_esc v
| C_uninit_noesc v
| C_init_esc v
@@ -737,7 +737,7 @@ module V_Or_Uninitialized = struct
| 3 -> C_init_noesc v
| _ -> assert false
-(* let (==>) = (fun x y -> (not x) || y) *)
+ (* let (==>) = (fun x y -> (not x) || y) *)
type size_widen_hint = V.size_widen_hint
type numerical_widen_hint = V.numerical_widen_hint
@@ -765,7 +765,7 @@ module V_Or_Uninitialized = struct
(V.link (get_v t1) (get_v t2))
let meet t1 t2 =
- create
+ create
((get_flags t1) lor (get_flags t2))
(V.meet (get_v t1) (get_v t2))
@@ -783,36 +783,36 @@ module V_Or_Uninitialized = struct
let initialized v = C_init_noesc v
let is_included t1 t2 =
-(* (t2.initialized ==> t1.initialized) &&
- (t2.no_escaping_adr ==> t1.no_escaping_adr) &&
- V.is_included t1.v t2.v
-*)
+ (* (t2.initialized ==> t1.initialized) &&
+ (t2.no_escaping_adr ==> t1.no_escaping_adr) &&
+ V.is_included t1.v t2.v
+ *)
let flags1 = get_flags t1 in
let flags2 = get_flags t2 in
(lnot flags2) lor flags1 = -1 &&
- V.is_included (get_v t1) (get_v t2)
+ V.is_included (get_v t1) (get_v t2)
let pretty_aux pp fmt t =
let no_escaping_adr = is_noesc t in
let initialized = is_initialized t in
let v = get_v t in
match V.(equal bottom v), initialized, no_escaping_adr with
- | false, false, false ->
- Format.fprintf fmt "%a or UNINITIALIZED or ESCAPINGADDR" pp v
- | true, false, false ->
- Format.pp_print_string fmt "UNINITIALIZED or ESCAPINGADDR"
- | false, false, true ->
- Format.fprintf fmt "%a or UNINITIALIZED" pp v
- | true, false, true ->
- Format.pp_print_string fmt "UNINITIALIZED"
- | false, true, false ->
- Format.fprintf fmt "%a or ESCAPINGADDR" pp v
- | true, true, false ->
- Format.pp_print_string fmt "ESCAPINGADDR"
- | false, true, true ->
- pp fmt v
- | true, true, true ->
- Format.pp_print_string fmt "BOTVALUE"
+ | false, false, false ->
+ Format.fprintf fmt "%a or UNINITIALIZED or ESCAPINGADDR" pp v
+ | true, false, false ->
+ Format.pp_print_string fmt "UNINITIALIZED or ESCAPINGADDR"
+ | false, false, true ->
+ Format.fprintf fmt "%a or UNINITIALIZED" pp v
+ | true, false, true ->
+ Format.pp_print_string fmt "UNINITIALIZED"
+ | false, true, false ->
+ Format.fprintf fmt "%a or ESCAPINGADDR" pp v
+ | true, true, false ->
+ Format.pp_print_string fmt "ESCAPINGADDR"
+ | false, true, true ->
+ pp fmt v
+ | true, true, true ->
+ Format.pp_print_string fmt "BOTVALUE"
let pretty fmt v = pretty_aux V.pretty fmt v
let pretty_typ typ fmt v =
@@ -828,38 +828,38 @@ module V_Or_Uninitialized = struct
include
(Datatype.Make
- (struct
- type uninitialized = t
- type t = uninitialized (* = | C_uninit_esc of V.t
- | C_uninit_noesc of V.t
- | C_init_esc of V.t
- | C_init_noesc of V.t *)
- let name = "Cvalue.V_Or_Uninitialized"
- let structural_descr =
- let v = V.packed_descr in
+ (struct
+ type uninitialized = t
+ type t = uninitialized (* = | C_uninit_esc of V.t
+ | C_uninit_noesc of V.t
+ | C_init_esc of V.t
+ | C_init_noesc of V.t *)
+ let name = "Cvalue.V_Or_Uninitialized"
+ let structural_descr =
+ let v = V.packed_descr in
Structural_descr.t_sum [| [| v |]; [| v |]; [| v |]; [| v |] |]
- let reprs =
- List.fold_left
- (fun acc v ->
- List.fold_left
- (fun acc v ->
- List.fold_left
- (fun acc v -> C_uninit_noesc v :: acc)
- (C_uninit_esc v :: acc)
- V.reprs)
- (C_init_noesc v :: acc)
- V.reprs)
- (List.map (fun v -> C_init_esc v) V.reprs)
- V.reprs
- let hash = hash
- let equal = equal
- let compare = Datatype.undefined
- let copy = Datatype.undefined
- let rehash = Datatype.identity
- let pretty = pretty
- let internal_pretty_code = Datatype.undefined
- let varname = Datatype.undefined
- let mem_project = Datatype.never_any_project
+ let reprs =
+ List.fold_left
+ (fun acc v ->
+ List.fold_left
+ (fun acc v ->
+ List.fold_left
+ (fun acc v -> C_uninit_noesc v :: acc)
+ (C_uninit_esc v :: acc)
+ V.reprs)
+ (C_init_noesc v :: acc)
+ V.reprs)
+ (List.map (fun v -> C_init_esc v) V.reprs)
+ V.reprs
+ let hash = hash
+ let equal = equal
+ let compare = Datatype.undefined
+ let copy = Datatype.undefined
+ let rehash = Datatype.identity
+ let pretty = pretty
+ let internal_pretty_code = Datatype.undefined
+ let varname = Datatype.undefined
+ let mem_project = Datatype.never_any_project
end)
: Datatype.S with type t := t)
@@ -998,7 +998,7 @@ module V_Offsetmap = struct
let narrow_reinterpret x y =
try `Value (OffsetmapNarrow.narrow_reinterpret x y)
with NarrowReturnsBottom -> `Bottom
-
+
end
module Default_offsetmap = struct
@@ -1007,10 +1007,10 @@ module Default_offsetmap = struct
State_builder.Int_hashtbl
(V_Offsetmap)
(struct
- let name = "Cvalue.Default_offsetmap.StringOffsetmaps"
- let dependencies = [ Ast.self ]
- let size = 17
- end)
+ let name = "Cvalue.Default_offsetmap.StringOffsetmaps"
+ let dependencies = [ Ast.self ]
+ let size = 17
+ end)
let () = Ast.add_monotonic_state StringOffsetmaps.self
let default_offsetmap base =
@@ -1046,7 +1046,7 @@ module Default_offsetmap = struct
sets of locals, but is is ok to have missing ones considered as being
bound to Bottom.
- for dynamic allocation, the default value is indeed Bottom
- *)
+ *)
let name = "Cvalue.Default_offsetmap"
@@ -1077,7 +1077,7 @@ module Model = struct
let reduce_indeterminate_binding state l v =
assert (Locations.cardinal_zero_or_one l);
add_binding ~exact:true state l v
-
+
(* Overwrites the definition of add_binding coming from Lmap, with a
signature change. *)
let add_binding ~exact acc loc value =
@@ -1087,18 +1087,18 @@ module Model = struct
List.fold_left
(fun acc block -> remove_variables block.blocals acc) state blocks
- let cardinal_estimate state =
- match state with
- | Bottom -> CardinalEstimate.zero
- | Top -> CardinalEstimate.infinite
- | Map(m) ->
- let count = ref (CardinalEstimate.one) in
- let f _ offsetmap =
- let offsetmap_card = V_Offsetmap.cardinal_estimate offsetmap in
- count := CardinalEstimate.mul !count offsetmap_card
- in
- iter f m;
- !count
+ let cardinal_estimate state =
+ match state with
+ | Bottom -> CardinalEstimate.zero
+ | Top -> CardinalEstimate.infinite
+ | Map(m) ->
+ let count = ref (CardinalEstimate.one) in
+ let f _ offsetmap =
+ let offsetmap_card = V_Offsetmap.cardinal_estimate offsetmap in
+ count := CardinalEstimate.mul !count offsetmap_card
+ in
+ iter f m;
+ !count
end
(*
diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli
index dc2f6ae7dd335273ae7014033fba9926c1cfb4e6..0b55de0ca3eea5e22593c6429141846bdc3f222e 100644
--- a/src/plugins/value_types/cvalue.mli
+++ b/src/plugins/value_types/cvalue.mli
@@ -26,7 +26,7 @@ open Abstract_interp
open Locations
(** Estimation of the cardinal of the concretization of an abstract state
- or value. *)
+ or value. *)
module CardinalEstimate: sig
type t
val one: t
@@ -45,15 +45,15 @@ module V : sig
(* Too many aliases, and OCaml module system is not able to keep track
of all of them. Use some shortcuts *)
with type M.t = Location_Bytes.M.t
- and type t = Location_Bytes.t
- and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
- and type size_widen_hint = Location_Bytes.size_widen_hint
+ and type t = Location_Bytes.t
+ and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
+ and type size_widen_hint = Location_Bytes.size_widen_hint
include module type of Offsetmap_lattice_with_isotropy
- with type t := t
- and type numerical_widen_hint := numerical_widen_hint
- and type size_widen_hint := size_widen_hint
- and type widen_hint := widen_hint
+ with type t := t
+ and type numerical_widen_hint := numerical_widen_hint
+ and type size_widen_hint := size_widen_hint
+ and type widen_hint := widen_hint
val pretty_typ: Cil_types.typ option -> t Pretty_utils.formatter
@@ -69,7 +69,7 @@ module V : sig
val project_ival_bottom: t -> Ival.t
(* Temporary API, will be merged with project_ival later *)
-
+
val is_imprecise : t -> bool
val is_topint : t -> bool
val is_bottom : t -> bool
@@ -95,12 +95,12 @@ module V : sig
val inject_float : Fval.t -> t
val interp_boolean : contains_zero:bool -> contains_non_zero:bool -> t
-(** [cast_int_to_int ~size ~signed v] applies to the abstract value [v] the
- conversion to the integer type described by [size] and [signed].
- Offsets of bases other than NULL are not clipped. If they were clipped,
- they should be clipped at the validity of the base. The C standard does
- not say that [p+(1ULL<<32+1)] is the same as [p+1], it says that
- [p+(1ULL<<32+1)] is invalid. *)
+ (** [cast_int_to_int ~size ~signed v] applies to the abstract value [v] the
+ conversion to the integer type described by [size] and [signed].
+ Offsets of bases other than NULL are not clipped. If they were clipped,
+ they should be clipped at the validity of the base. The C standard does
+ not say that [p+(1ULL<<32+1)] is the same as [p+1], it says that
+ [p+(1ULL<<32+1)] is invalid. *)
val cast_int_to_int: size:Int.t -> signed:bool -> t -> t
val reinterpret_as_float: Cil_types.fkind -> t -> t
@@ -174,9 +174,9 @@ module V_Or_Uninitialized : sig
include module type of Offsetmap_lattice_with_isotropy
with type t := t
- and type size_widen_hint = Location_Bytes.size_widen_hint
- and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
- and type widen_hint = Locations.Location_Bytes.widen_hint
+ and type size_widen_hint = Location_Bytes.size_widen_hint
+ and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
+ and type widen_hint = Locations.Location_Bytes.widen_hint
include Lattice_type.With_Under_Approximation with type t:= t
include Lattice_type.With_Narrow with type t := t
include Lattice_type.With_Top with type t := t
@@ -212,32 +212,32 @@ module V_Or_Uninitialized : sig
val reduce_by_initializedness : bool -> t -> t
(** [reduce_by_initializedness initialized v] reduces [v] so that its result
- [r] verifies [\initialized(r)] if [initialized] is [true], and
- [!\initialized(r)] otherwise. *)
+ [r] verifies [\initialized(r)] if [initialized] is [true], and
+ [!\initialized(r)] otherwise. *)
val reduce_by_danglingness : bool -> t -> t
(** [reduce_by_danglingness dangling v] reduces [v] so that its result [r]
- verifies [\dangling(r)] if [dangling] is [true], and
- [!\dangling(r)] otherwise. *)
+ verifies [\dangling(r)] if [dangling] is [true], and
+ [!\dangling(r)] otherwise. *)
val remove_indeterminateness: t -> t
(** Remove 'uninitialized' and 'escaping addresses' flags from the argument *)
- val unspecify_escaping_locals :
+ val unspecify_escaping_locals :
exact:bool -> (V.M.key -> bool) -> t -> bool * t
val map: (V.t -> V.t) -> t -> t
val map2: (V.t -> V.t -> V.t) -> t -> t -> t
(** initialized/escaping information is the join of the information
on each argument. *)
- end
+end
(** Memory slices. They are maps from intervals to values with
flags. All sizes and intervals are in bits. *)
module V_Offsetmap: sig
include module type of Offsetmap_sig
- with type v = V_Or_Uninitialized.t
- and type widen_hint = V_Or_Uninitialized.numerical_widen_hint
+ with type v = V_Or_Uninitialized.t
+ and type widen_hint = V_Or_Uninitialized.numerical_widen_hint
val narrow: t -> t -> t Bottom.Type.or_bottom
val narrow_reinterpret: t -> t -> t Bottom.Type.or_bottom
@@ -256,8 +256,8 @@ module Model: sig
(** Functions inherited from [Lmap_sig] interface *)
include module type of Lmap_sig
with type v = V_Or_Uninitialized.t
- and type offsetmap = V_Offsetmap.t
- and type widen_hint_base = V_Or_Uninitialized.numerical_widen_hint
+ and type offsetmap = V_Offsetmap.t
+ and type widen_hint_base = V_Or_Uninitialized.numerical_widen_hint
include Lattice_type.With_Narrow with type t := t
@@ -279,6 +279,7 @@ module Model: sig
- if [conflate_bottom] is [false] and at least one bit pointed to by
[l..l+loc.size-1] is not [V.bottom], the value is an approximation
of the join of all the bits at [l..l+loc.size-1].
+
As a rule of thumb, you must set [conflate_bottom=true] when the
operation you abstract really accesses [loc.size] bits, and when
undeterminate values are an error. This is typically the case when
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index a6c0564503dce968927047a94e514f5fc6ae08c7..9a8ae91a6f8df6215975b01ba810759f1e532a2b 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -867,7 +867,7 @@ let dump () =
in Format.fprintf fmt "@[<hv 0>Init:@ %a@]@." E.pretty a_init ;
KFmap.iter (fun kf m ->
(* Do not dump results for frama-c builtins *)
- if not (Cil.is_builtin (Kernel_function.get_vi kf)) then
+ if not (Cil_builtins.is_builtin (Kernel_function.get_vi kf)) then
Format.fprintf fmt "@[<hv 0>Function %a:@ %a@]@."
Kernel_function.pretty kf E.pretty m ;
) a_usage;
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index cb2d079f01617cb9654a9320702f8fe1cab9adf9..245096cde6f403c2e4032d8f8b74a0efd38e50cb 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -464,7 +464,7 @@ let bits_sizeof_comp cinfo = Cil.bitsSizeOf (typ_comp cinfo)
let bits_sizeof_array ainfo =
match ainfo.arr_flat with
| Some a ->
- let csize = Cil.integer ~loc:Cil.builtinLoc a.arr_cell_nbr in
+ let csize = Cil.integer ~loc:Cil_builtins.builtinLoc a.arr_cell_nbr in
let ctype = TArray(a.arr_cell,Some csize,Cil.empty_size_cache(),[]) in
Cil.bitsSizeOf ctype
| None ->
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cint.mlw b/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
index 2a8e1c460523dc755e0fff4f132f7358d51ead8b..969326b6fe91bdce835b6efaa34b84929f0936da 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
@@ -102,14 +102,14 @@ theory Cint
meta "remove_for_" lemma is_to_uint
meta "remove_for_" lemma is_to_sint
- axiom is_to_uint8 : forall x:int [ is_uint8(to_uint8 x) ]. is_uint8 (to_uint8 x)
- axiom is_to_sint8 : forall x:int [ is_sint8(to_sint8 x) ]. is_sint8 (to_sint8 x)
- axiom is_to_uint16 : forall x:int [ is_uint16(to_uint16 x) ]. is_uint16 (to_uint16 x)
- axiom is_to_sint16 : forall x:int [ is_sint16(to_sint16 x) ]. is_sint16 (to_sint16 x)
- axiom is_to_uint32 : forall x:int [ is_uint32(to_uint32 x) ]. is_uint32 (to_uint32 x)
- axiom is_to_sint32 : forall x:int [ is_sint32(to_sint32 x) ]. is_sint32 (to_sint32 x)
- axiom is_to_uint64 : forall x:int [ is_uint64(to_uint64 x) ]. is_uint64 (to_uint64 x)
- axiom is_to_sint64 : forall x:int [ is_sint64(to_sint64 x) ]. is_sint64 (to_sint64 x)
+ axiom is_to_uint8 : forall x:int. is_uint8 (to_uint8 x)
+ axiom is_to_sint8 : forall x:int. is_sint8 (to_sint8 x)
+ axiom is_to_uint16 : forall x:int. is_uint16 (to_uint16 x)
+ axiom is_to_sint16 : forall x:int. is_sint16 (to_sint16 x)
+ axiom is_to_uint32 : forall x:int. is_uint32 (to_uint32 x)
+ axiom is_to_sint32 : forall x:int. is_sint32 (to_sint32 x)
+ axiom is_to_uint64 : forall x:int. is_uint64 (to_uint64 x)
+ axiom is_to_sint64 : forall x:int. is_sint64 (to_sint64 x)
(** * C-Integer Conversions are identity when in-range * **)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d2b0d3de19a44706760e2805d7c14e3c949490cf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
@@ -0,0 +1,106 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/overflow2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function pointers_and_companions
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'pointers_and_companions':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a01' (file tests/wp_plugin/overflow2.c, line 20):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a02' (file tests/wp_plugin/overflow2.c, line 21):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a03' (file tests/wp_plugin/overflow2.c, line 22):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a04' (file tests/wp_plugin/overflow2.c, line 23):
+Assume {
+ Type: is_sint16(distance_0) /\ is_uint32(p1_off_0).
+ (* Pre-condition *)
+ Have: p1_off_0 <= 10.
+}
+Prove: (p1_off_0 + to_uint16(distance_0)) <= 65545.
+
+------------------------------------------------------------
+
+Goal Assertion 'a05' (file tests/wp_plugin/overflow2.c, line 24):
+Let x = p1_off_0 + to_uint16(distance_0).
+Assume {
+ Type: is_sint16(distance_0) /\ is_uint32(p1_off_0).
+ (* Pre-condition *)
+ Have: p1_off_0 <= 10.
+ (* Assertion 'a04' *)
+ Have: x <= 65545.
+}
+Prove: x = to_uint32(x).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/overflow2.c, line 14) in 'pointers_and_companions':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function pointers_and_companions_ulong
+------------------------------------------------------------
+
+Goal Post-condition 'postul' in 'pointers_and_companions_ulong':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a06' (file tests/wp_plugin/overflow2.c, line 39):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a07' (file tests/wp_plugin/overflow2.c, line 40):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a08' (file tests/wp_plugin/overflow2.c, line 41):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a09' (file tests/wp_plugin/overflow2.c, line 42):
+Assume {
+ Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
+ (* Pre-condition *)
+ Have: p1_off_alt_0 <= 10.
+}
+Prove: (p1_off_alt_0 + to_uint16(distance_0)) <= 65545.
+
+------------------------------------------------------------
+
+Goal Assertion 'a10' (file tests/wp_plugin/overflow2.c, line 43):
+Let x = p1_off_alt_0 + to_uint16(distance_0).
+Assume {
+ Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
+ (* Pre-condition *)
+ Have: p1_off_alt_0 <= 10.
+ (* Assertion 'a09' *)
+ Have: x <= 65545.
+}
+Prove: x = to_uint32(x).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/overflow2.c, line 33) in 'pointers_and_companions_ulong':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9c2dfad26f93af7de878b0d812d73f6cfaefc23d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overflow2.res.oracle
@@ -0,0 +1,27 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/overflow2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 14 goals scheduled
+[wp] [Qed] Goal typed_pointers_and_companions_ensures_post : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_assert_a01 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_assert_a02 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_assert_a03 : Valid
+[wp] [Alt-Ergo] Goal typed_pointers_and_companions_assert_a04 : Valid
+[wp] [Alt-Ergo] Goal typed_pointers_and_companions_assert_a05 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_assigns : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_ensures_postul : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_assert_a06 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_assert_a07 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_assert_a08 : Valid
+[wp] [Alt-Ergo] Goal typed_pointers_and_companions_ulong_assert_a09 : Valid
+[wp] [Alt-Ergo] Goal typed_pointers_and_companions_ulong_assert_a10 : Valid
+[wp] [Qed] Goal typed_pointers_and_companions_ulong_assigns : Valid
+[wp] Proved goals: 14 / 14
+ Qed: 10
+ Alt-Ergo: 4
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ pointers_and_companions 5 2 7 100%
+ pointers_and_companions_ulong 5 2 7 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/overflow2.c b/src/plugins/wp/tests/wp_plugin/overflow2.c
new file mode 100644
index 0000000000000000000000000000000000000000..f2a27e3b194a6c9b7d4b28557390cf44a082e05a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/overflow2.c
@@ -0,0 +1,44 @@
+/* run with: frama-c-gui -wp -wp-rte strange_work_again.c */
+// uproven: a04, a05, a09, a10
+// note that when the type of distance is ushort, all is proven
+
+typedef unsigned char uchar;
+typedef unsigned short ushort;
+typedef unsigned int uint;
+typedef unsigned long ulong;
+
+uint p1_off, p2_off;
+
+/*@
+ requires p1_off <= 10;
+ assigns p2_off;
+ ensures post: p2_off == p1_off + (ushort)distance;
+*/
+void pointers_and_companions(short distance)
+{
+ p2_off = p1_off + (ushort)distance;
+ //@ assert a01: p2_off == (uint)(p1_off + (ushort)distance);
+ //@ assert a02: (ushort)distance <= 65535;
+ //@ assert a03: p1_off <= 10;
+ //@ assert a04: p1_off + (ushort)distance <= 10 + 65535;
+ //@ assert a05: p1_off + (ushort)distance == (uint)(p1_off + (ushort)distance);
+}
+
+// the same behavior for ulong
+
+ulong p1_off_alt, p2_off_alt;
+
+/*@
+ requires p1_off_alt <= 10;
+ assigns p2_off_alt;
+ ensures postul: p2_off_alt == p1_off_alt + (ushort)distance;
+*/
+void pointers_and_companions_ulong(short distance)
+{
+ p2_off_alt = p1_off_alt + (ushort)distance;
+ //@ assert a06: p2_off_alt == (uint)(p1_off_alt + (ushort)distance);
+ //@ assert a07: (ushort)distance <= 65535;
+ //@ assert a08: p1_off_alt <= 10;
+ //@ assert a09: p1_off_alt + (ushort)distance <= 10 + 65535;
+ //@ assert a10: ((ulong)(p1_off_alt + (ushort)distance)) == (p1_off_alt + (ushort)distance);
+}
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index a9310f3d13966a1a1a987551a3cfb57c72a1e8cd..347be3b9000ef396daebdf2335c9f2fbaad88a84 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0236,
+ "verdict": "valid", "time": 0.0241,
"steps": 41 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0251,
+ "verdict": "valid", "time": 0.025,
"steps": 41 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index a5b7496b8bcac1057fc2ee1bfc1baa80fad18099..a5416d5a156584963cf2cf5bcc42ebfb7e27b602 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.018,
+ "verdict": "valid", "time": 0.0199,
"steps": 29 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.022,
+ "verdict": "valid", "time": 0.0241,
"steps": 29 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
index 6defa5bcd74401f918dc86a7cc117daec22e3cc0..6a684ed4e4fa19eaae36dd09d3b7717df0c65a0e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -3,7 +3,7 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0177,
+ "verdict": "valid", "time": 0.0202,
"steps": 40 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0177,
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
index 07c88e21be0523b36d4e4beb3bc08582fc5171d3..578ffb9958aef6bacf33cb5680b0ecbafe0f5efe 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E$i0$i$j$j9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0154,
+ "verdict": "valid", "time": 0.0143,
"steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0157,
+ "verdict": "valid", "time": 0.0146,
"steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
index 6f266473c3da74f3125a63e16abeffe0f28b841c..72b93b5526df3a049e39f88a0d1809d9e3ec6941 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0167,
+ "verdict": "valid", "time": 0.016,
"steps": 33 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0171,
+ "verdict": "valid", "time": 0.0161,
"steps": 33 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
index 33301d71a33e5ae00a155943d5cecf22939281b0..09755e2c851424c8871e943d93a05b0253bf1db9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0167,
+ "verdict": "valid", "time": 0.016,
"steps": 33 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0171,
+ "verdict": "valid", "time": 0.0161,
"steps": 33 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
index b729e0fa94298a8357840d6070954d28886407f2..706eac2712b2643fdff1c6caaea6ca9725f711ad 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0169,
+ "verdict": "valid", "time": 0.0209,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0167,
+ "verdict": "valid", "time": 0.0184,
"steps": 39 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
index 2580abd19c2c0e2e65e4a8eab92f30bf4b298b28..d035bcd5046d5abb9450a6bd66795f980f87369f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -6,5 +6,5 @@
"verdict": "valid", "time": 0.0146,
"steps": 27 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0146,
+ "verdict": "valid", "time": 0.0143,
"steps": 27 } ] } } ]
diff --git a/tests/cil/Change_formals.ml b/tests/cil/Change_formals.ml
index c311efe0728a4444f2451e7db30ddba4ee6c96e9..3ed509cbbe9a90d0a789d62f77eacd24e0df3140 100644
--- a/tests/cil/Change_formals.ml
+++ b/tests/cil/Change_formals.ml
@@ -32,7 +32,7 @@ class transform prj = object(_self)
let mk_gvar_decl = function l ->
begin match l with
| (GFunDecl (_fspec, vi, _loc) as g) :: [] ->
- if not (Cil.Frama_c_builtins.mem vi.vname) then
+ if not (Cil_builtins.Frama_c_builtins.mem vi.vname) then
begin match vi.vtype with
| TFun(typ, args, varity, attr) ->
let vtype = Cil.argsToList args in
diff --git a/tests/fc_script/make-for-make-wrapper.mk b/tests/fc_script/make-for-make-wrapper.mk
new file mode 100644
index 0000000000000000000000000000000000000000..983f2a16d9f1be8dcaaaa332626afa7c6c54ffee
--- /dev/null
+++ b/tests/fc_script/make-for-make-wrapper.mk
@@ -0,0 +1,22 @@
+# Customized makefile template for testing 'frama-c-script make-wrapper'.
+
+include $(shell $(FRAMAC) -no-autoload-plugins -print-share-path)/analysis-scripts/prologue.mk
+
+FCFLAGS += \
+ -kernel-warn-key annot:missing-spec=abort \
+ -kernel-warn-key typing:implicit-function-declaration=abort \
+
+EVAFLAGS += \
+ -eva-warn-key builtins:missing-spec=abort \
+
+## Analysis targets (suffixed with .eva)
+TARGETS = make-for-make-wrapper.eva
+
+make-for-make-wrapper.parse: \
+ make-wrapper.c \
+ make-wrapper2.c \
+ # make-wrapper3.c is deliberately absent of this list
+
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC) -no-autoload-plugins -print-share-path)/analysis-scripts/epilogue.mk
+###############################################################################
diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.c
new file mode 100644
index 0000000000000000000000000000000000000000..cc36eead6f02ea799797df57409233db946e5658
--- /dev/null
+++ b/tests/fc_script/make-wrapper.c
@@ -0,0 +1,18 @@
+/* run.config
+ NOFRAMAC: testing frama-c-script
+ COMMENT: we must filter 'make:' output lines, since they differ when run by the CI (e.g. mention to jobserver)
+ EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && FRAMAC=../../bin/frama-c ../../bin/frama-c-script make-wrapper --make-dir . -f make-for-make-wrapper.mk | sed -e "s:$PWD:PWD:g" | grep -v "^make.*" > result/make-wrapper.res 2> result/make-wrapper.err && rm -rf make-for-make-wrapper.parse make-for-make-wrapper.eva
+*/
+
+int defined(int a);
+
+int specified(int a);
+
+int external(int a);
+
+int main() {
+ int a = 42;
+ a = defined(a);
+ a = specified(a);
+ a = external(a);
+}
diff --git a/tests/fc_script/make-wrapper2.c b/tests/fc_script/make-wrapper2.c
new file mode 100644
index 0000000000000000000000000000000000000000..0f97864c1b8f7a6192590aa232ac04e7e4ca3090
--- /dev/null
+++ b/tests/fc_script/make-wrapper2.c
@@ -0,0 +1,16 @@
+/* run.config
+ DONTRUN: part of the test in make-wrapper.c
+*/
+
+int defined(int a) {
+ return a + 1;
+}
+
+/*@
+ assigns \result \from a;
+ ensures \result == a + 2;
+ */
+int specified(int a);
+
+// defined in another, non-included, file
+int external(int a);
diff --git a/tests/fc_script/make-wrapper3.c b/tests/fc_script/make-wrapper3.c
new file mode 100644
index 0000000000000000000000000000000000000000..83ed541f1db724dc886d6bb865491c47d866d0e2
--- /dev/null
+++ b/tests/fc_script/make-wrapper3.c
@@ -0,0 +1,9 @@
+/* run.config
+ DONTRUN: part of the test in make-wrapper.c
+*/
+
+// This file contains a definition for function 'external', but it is _not_
+// included when parsing 'make-wrapper.c'. This triggers a make-wrapper message.
+int external(int a) {
+ return a + 3;
+}
diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res
index a846b6beb54f9a0245507e35df7567e3d48e9245..3e35782af42a6f5546e034e026a63d09df5ac934 100644
--- a/tests/fc_script/oracle/find_fun1.res
+++ b/tests/fc_script/oracle/find_fun1.res
@@ -1,4 +1,4 @@
-Looking for 'main2' inside 5 file(s)...
+Looking for 'main2' inside 8 file(s)...
Possible declarations for function 'main2' in the following file(s):
tests/fc_script/for-find-fun.c
Possible definitions for function 'main2' in the following file(s):
diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res
index 273cc015b4ef5f5ef497533511f083c50c2c63fe..e9f42fdf76a5d227ee458abdc59e3370a26d57d1 100644
--- a/tests/fc_script/oracle/find_fun2.res
+++ b/tests/fc_script/oracle/find_fun2.res
@@ -1,4 +1,4 @@
-Looking for 'main3' inside 5 file(s)...
+Looking for 'main3' inside 8 file(s)...
Possible declarations for function 'main3' in the following file(s):
tests/fc_script/for-find-fun2.c
Possible definitions for function 'main3' in the following file(s):
diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res
index a7059bd1c963ad064b030a17ef9782873c397b0d..65fc349325d2406ea212025ed38e51347b09217f 100644
--- a/tests/fc_script/oracle/find_fun3.res
+++ b/tests/fc_script/oracle/find_fun3.res
@@ -1,2 +1,2 @@
-Looking for 'false_positive' inside 5 file(s)...
+Looking for 'false_positive' inside 8 file(s)...
No declaration/definition found for function 'false_positive'
diff --git a/tests/fc_script/oracle/make-wrapper.err b/tests/fc_script/oracle/make-wrapper.err
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
new file mode 100644
index 0000000000000000000000000000000000000000..9faa818ae65c5e1aa39fdd07142c63896fb6e6cc
--- /dev/null
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -0,0 +1,26 @@
+
+[34mCommand: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -cpp-extra-args="" make-wrapper.c make-wrapper2.c(B[m
+
+[kernel] Parsing make-wrapper.c (with preprocessing)
+[kernel] Parsing make-wrapper2.c (with preprocessing)
+
+[34mCommand: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort (B[m
+
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] using specification for function specified
+[kernel:annot:missing-spec] make-wrapper.c:17: Warning:
+ Neither code nor specification for function external, generating default assigns from the prototype
+[kernel] User Error: warning annot:missing-spec treated as fatal error.
+[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'.
+
+***** make-wrapper recommendations *****
+
+*** recommendation #1 ***
+
+1. Found function with missing spec: external
+ Looking for files defining it...
+Add the following file to the list of sources to be parsed:
+ make-wrapper3.c
diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml
index 259c2fe8abac993c14b817353eeecd44dbace5dd..d2319d0f4b81a02e3a66d55474e63ea4e882c3d7 100644
--- a/tests/misc/bts1347.ml
+++ b/tests/misc/bts1347.ml
@@ -5,7 +5,7 @@ let emitter =
let run () =
Globals.Functions.iter
(fun kf ->
- if not (Cil.is_builtin (Kernel_function.get_vi kf)) then begin
+ if not (Cil_builtins.is_builtin (Kernel_function.get_vi kf)) then begin
Globals.set_entry_point (Kernel_function.get_name kf) true;
!Db.Value.compute();
let hyps =
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 091c7d8002d8a53274789b3887edaaec956ffbe2..510a8f2b3ab41a3c39cd5c26cc41c8703528b9e1 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -2,6 +2,8 @@
[kernel:file:print-one]
result of parsing tests/syntax/check_builtin_bts1440.i:
/* Generated by Frama-C */
+ void __builtin__Exit(int);
+
int __builtin___fprintf_chk(void *, int, char const * , ...);
void *__builtin___memcpy_chk(void *, void const *, unsigned int, unsigned int);
@@ -43,10 +45,18 @@
int __builtin___vsprintf_chk(char *, int, unsigned int, char const *,
__builtin_va_list);
+ int __builtin_abs(int);
+
double __builtin_acos(double);
float __builtin_acosf(float);
+ double __builtin_acosh(double);
+
+ float __builtin_acoshf(float);
+
+ long double __builtin_acoshl(long double);
+
long double __builtin_acosl(long double);
void *__builtin_alloca(unsigned int);
@@ -55,6 +65,12 @@
float __builtin_asinf(float);
+ double __builtin_asinh(double);
+
+ float __builtin_asinhf(float);
+
+ long double __builtin_asinhl(long double);
+
long double __builtin_asinl(long double);
double __builtin_atan(double);
@@ -67,6 +83,12 @@
float __builtin_atanf(float);
+ double __builtin_atanh(double);
+
+ float __builtin_atanhf(float);
+
+ long double __builtin_atanhl(long double);
+
long double __builtin_atanl(long double);
unsigned short __builtin_bswap16(unsigned short);
@@ -75,6 +97,14 @@
unsigned long long __builtin_bswap64(unsigned long long);
+ void *__builtin_calloc(unsigned int, unsigned int);
+
+ double __builtin_cbrt(double);
+
+ float __builtin_cbrtf(float);
+
+ long double __builtin_cbrtl(long double);
+
double __builtin_ceil(double);
float __builtin_ceilf(float);
@@ -83,6 +113,12 @@
int __builtin_constant_p(int);
+ double __builtin_copysign(double, double);
+
+ float __builtin_copysignf(float, float);
+
+ long double __builtin_copysignl(long double, long double);
+
double __builtin_cos(double);
float __builtin_cosf(float);
@@ -95,20 +131,52 @@
long double __builtin_cosl(long double);
+ double __builtin_erf(double);
+
+ double __builtin_erfc(double);
+
+ float __builtin_erfcf(float);
+
+ long double __builtin_erfcl(long double);
+
+ float __builtin_erff(float);
+
+ long double __builtin_erfl(long double);
+
+ void __builtin_exit(int);
+
double __builtin_exp(double);
+ double __builtin_exp2(double);
+
+ float __builtin_exp2f(float);
+
+ long double __builtin_exp2l(long double);
+
long __builtin_expect(long, long);
float __builtin_expf(float);
long double __builtin_expl(long double);
+ double __builtin_expm1(double);
+
+ float __builtin_expm1f(float);
+
+ long double __builtin_expm1l(long double);
+
double __builtin_fabs(double);
float __builtin_fabsf(float);
long double __builtin_fabsl(long double);
+ double __builtin_fdim(double, double);
+
+ float __builtin_fdimf(float, float);
+
+ long double __builtin_fdiml(long double, long double);
+
int __builtin_ffs(unsigned int);
int __builtin_ffsl(unsigned long);
@@ -121,44 +189,128 @@
long double __builtin_floorl(long double);
+ double __builtin_fma(double, double, double);
+
+ float __builtin_fmaf(float, float, float);
+
+ long double __builtin_fmal(long double, long double, long double);
+
+ double __builtin_fmax(double, double);
+
+ float __builtin_fmaxf(float, float);
+
+ long double __builtin_fmaxl(long double, long double);
+
+ double __builtin_fmin(double, double);
+
+ float __builtin_fminf(float, float);
+
+ long double __builtin_fminl(long double, long double);
+
double __builtin_fmod(double);
float __builtin_fmodf(float);
long double __builtin_fmodl(long double);
+ int __builtin_fprintf(void *, char const * , ...);
+
+ int __builtin_fputs(char const *, void *);
+
void *__builtin_frame_address(unsigned int);
+ void __builtin_free(void *);
+
double __builtin_frexp(double, int *);
float __builtin_frexpf(float, int *);
long double __builtin_frexpl(long double, int *);
+ int __builtin_fscanf(void *, char const * , ...);
+
double __builtin_huge_val(void);
float __builtin_huge_valf(void);
long double __builtin_huge_vall(void);
+ double __builtin_hypot(double, double);
+
+ float __builtin_hypotf(float, float);
+
+ long double __builtin_hypotl(long double, long double);
+
void __builtin_ia32_lfence(void);
void __builtin_ia32_mfence(void);
void __builtin_ia32_sfence(void);
+ double __builtin_ilogb(double);
+
+ float __builtin_ilogbf(float);
+
+ long double __builtin_ilogbl(long double);
+
double __builtin_inf(void);
float __builtin_inff(void);
long double __builtin_infl(void);
+ int __builtin_isalnum(int);
+
+ int __builtin_isalpha(int);
+
+ int __builtin_isblank(int);
+
+ int __builtin_iscntrl(int);
+
+ int __builtin_isdigit(int);
+
+ int __builtin_isgraph(int);
+
+ int __builtin_islower(int);
+
+ int __builtin_isprint(int);
+
+ int __builtin_ispunct(int);
+
+ int __builtin_isspace(int);
+
+ int __builtin_isupper(int);
+
+ int __builtin_isxdigit(int);
+
+ long __builtin_labs(long);
+
double __builtin_ldexp(double, int);
float __builtin_ldexpf(float, int);
long double __builtin_ldexpl(long double, int);
+ double __builtin_lgamma(double);
+
+ float __builtin_lgammaf(float);
+
+ long double __builtin_lgammal(long double);
+
+ long long __builtin_llabs(long long);
+
+ long long __builtin_llrint(double);
+
+ long long __builtin_llrintf(float);
+
+ long long __builtin_llrintl(long double);
+
+ long long __builtin_llround(double);
+
+ long long __builtin_llroundf(float);
+
+ long long __builtin_llroundl(long double);
+
double __builtin_log(double);
double __builtin_log10(double);
@@ -167,15 +319,53 @@
long double __builtin_log10l(long double);
+ double __builtin_log1p(double);
+
+ float __builtin_log1pf(float);
+
+ long double __builtin_log1pl(long double);
+
+ double __builtin_log2(double);
+
+ float __builtin_log2f(float);
+
+ long double __builtin_log2l(long double);
+
+ double __builtin_logb(double);
+
+ float __builtin_logbf(float);
+
+ long double __builtin_logbl(long double);
+
float __builtin_logf(float);
long double __builtin_logl(long double);
+ long __builtin_lrint(double);
+
+ long __builtin_lrintf(float);
+
+ long __builtin_lrintl(long double);
+
+ long __builtin_lround(double);
+
+ long __builtin_lroundf(float);
+
+ long __builtin_lroundl(long double);
+
+ void *__builtin_malloc(unsigned int);
+
+ void *__builtin_memchr(void const *, int, unsigned int);
+
+ int __builtin_memcmp(void const *, void const *, unsigned int);
+
void *__builtin_memcpy(void *, void const *, unsigned int);
void *__builtin_mempcpy(void *, void const *, unsigned int);
- void *__builtin_memset(void *, int, int);
+ void *__builtin_memset(void *, int, unsigned int);
+
+ double __builtin_modf(double, double *);
float __builtin_modff(float, float *);
@@ -193,8 +383,26 @@
long double __builtin_nansl(char const *);
+ double __builtin_nearbyint(double);
+
+ float __builtin_nearbyintf(float);
+
+ long double __builtin_nearbyintl(long double);
+
__builtin_va_list __builtin_next_arg(void);
+ double __builtin_nextafter(double, double);
+
+ float __builtin_nextafterf(float, float);
+
+ long double __builtin_nextafterl(long double, long double);
+
+ double __builtin_nexttoward(double, long double);
+
+ float __builtin_nexttowardf(float, long double);
+
+ long double __builtin_nexttowardl(long double, long double);
+
unsigned int __builtin_object_size(void *, int);
unsigned int __builtin_offsetof(unsigned int);
@@ -205,18 +413,70 @@
int __builtin_parityll(unsigned long long);
+ double __builtin_pow(double, double);
+
+ float __builtin_powf(float, float);
+
double __builtin_powi(double, int);
float __builtin_powif(float, int);
long double __builtin_powil(long double, int);
+ long double __builtin_powl(long double, long double);
+
void __builtin_prefetch(void const * , ...);
+ int __builtin_printf(char const * , ...);
+
+ int __builtin_putchar(int);
+
+ int __builtin_puts(char const *);
+
+ void *__builtin_realloc(void *, unsigned int);
+
+ double __builtin_remainder(double, double);
+
+ float __builtin_remainderf(float, float);
+
+ long double __builtin_remainderl(long double, long double);
+
+ double __builtin_remquo(double, double, int *);
+
+ float __builtin_remquof(float, float, int *);
+
+ long double __builtin_remquol(long double, long double, int *);
+
void __builtin_return(void const *);
void *__builtin_return_address(unsigned int);
+ double __builtin_rint(double);
+
+ float __builtin_rintf(float);
+
+ long double __builtin_rintl(long double);
+
+ double __builtin_round(double);
+
+ float __builtin_roundf(float);
+
+ long double __builtin_roundl(long double);
+
+ double __builtin_scalbln(double, long);
+
+ float __builtin_scalblnf(float, long);
+
+ long double __builtin_scalblnl(long double, long);
+
+ double __builtin_scalbn(double, int);
+
+ float __builtin_scalbnf(float, int);
+
+ long double __builtin_scalbnl(long double, int);
+
+ int __builtin_scanf(char const * , ...);
+
double __builtin_sin(double);
float __builtin_sinf(float);
@@ -229,16 +489,24 @@
long double __builtin_sinl(long double);
+ int __builtin_snprintf(char *, unsigned int, char const * , ...);
+
+ int __builtin_sprintf(char *, char const * , ...);
+
double __builtin_sqrt(double);
float __builtin_sqrtf(float);
long double __builtin_sqrtl(long double);
+ int __builtin_sscanf(char const *, char const * , ...);
+
void __builtin_stdarg_start(__builtin_va_list);
char *__builtin_stpcpy(char *, char const *);
+ char *__builtin_strcat(char *, char const *);
+
char *__builtin_strchr(char *, int);
int __builtin_strcmp(char const *, char const *);
@@ -247,6 +515,8 @@
unsigned int __builtin_strcspn(char const *, char const *);
+ unsigned int __builtin_strlen(char const *);
+
char *__builtin_strncat(char *, char const *, unsigned int);
int __builtin_strncmp(char const *, char const *, unsigned int);
@@ -255,8 +525,12 @@
char *__builtin_strpbrk(char const *, char const *);
+ char *__builtin_strrchr(char const *, int);
+
unsigned int __builtin_strspn(char const *, char const *);
+ char *__builtin_strstr(char const *, char const *);
+
double __builtin_tan(double);
float __builtin_tanf(float);
@@ -269,6 +543,22 @@
long double __builtin_tanl(long double);
+ double __builtin_tgamma(double);
+
+ float __builtin_tgammaf(float);
+
+ long double __builtin_tgammal(long double);
+
+ int __builtin_tolower(int);
+
+ int __builtin_toupper(int);
+
+ double __builtin_trunc(double);
+
+ float __builtin_truncf(float);
+
+ long double __builtin_truncl(long double);
+
int __builtin_types_compatible_p(unsigned int, unsigned int);
void __builtin_unreachable(void);
@@ -283,6 +573,20 @@
void __builtin_varargs_start(__builtin_va_list);
+ int __builtin_vfprintf(void *, char const *, __builtin_va_list);
+
+ int __builtin_vfscanf(void *, char const *, __builtin_va_list);
+
+ int __builtin_vprintf(char const *, __builtin_va_list);
+
+ int __builtin_vscanf(char const *, __builtin_va_list);
+
+ int __builtin_vsnprintf(char *, unsigned int, char const *, __builtin_va_list);
+
+ int __builtin_vsprintf(char *, char const *, __builtin_va_list);
+
+ int __builtin_vsscanf(char const *, char const *, __builtin_va_list);
+
short __sync_add_and_fetch_int16_t(short volatile *, short , ...);
int __sync_add_and_fetch_int32_t(int volatile *, int , ...);