Skip to content

GitLab

Commit 1e2d688a authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Cleaning code and update README

parent a69d61c3
Hide whitespace changes
Inline Side-by-side
Showing with 172 additions and 159 deletions
README.md
View file @ 1e2d688a
# MAIN README
Paparazzi UAS
=============
Frama-C Verification of Paparazzi
=================================
This GitLab project is a fork of Paparazzi UAV autopilot
(https://github.com/paparazzi/paparazzi) that verify
`pprz_algebra` library using Frama-C.
[![Build Status](https://travis-ci.org/paparazzi/paparazzi.png?branch=master)](https://travis-ci.org/paparazzi/paparazzi) [![Gitter chat](https://badges.gitter.im/paparazzi/discuss.svg)](https://gitter.im/paparazzi/discuss)
[![Codacy Badge](https://api.codacy.com/project/badge/Grade/811c4398588f435fa8bc926f53d40e9f)](https://app.codacy.com/app/gautierhattenberger/paparazzi?utm_source=github.com&utm_medium=referral&utm_content=paparazzi/paparazzi&utm_campaign=Badge_Grade_Dashboard)
<a href="https://scan.coverity.com/projects/paparazzi-paparazzi">
<img alt="Coverity Scan Build Status"
src="https://scan.coverity.com/projects/4928/badge.svg"/>
</a>
Paparazzi is a free open source software package for Unmanned (Air) Vehicle Systems.
For many years, the system has been used successfuly by hobbyists, universities and companies all over the world, on vehicles of various sizes (11.9g to 25kg).
Paparazzi supports fixed wing, rotorcraft, hybrids, flapping vehicles and it is even possible to use it for boats and surface vehicles.
Up to date information is available on the wiki http://wiki.paparazziuav.org
To get in touch, subscribe to the mailing list [paparazzi-devel@nongnu.org] (http://savannah.nongnu.org/mail/?group=paparazzi), the IRC channel (freenode, #paparazzi) and Gitter (https://gitter.im/paparazzi/discuss).
This project adds the ACSL annotations in the code and provide a
script to automatically launch the verification. Frama-C
analyses the code and checks the absence of RTE (_RunTime
Errors_) and some functional properties.
Required software
-----------------
Instructions for installation can be found on the wiki (http://wiki.paparazziuav.org/wiki/Installation).
For Ubuntu users, required packages are available in the [paparazzi-uav PPA] (https://launchpad.net/~paparazzi-uav/+archive/ppa),
Debian users can use the [OpenSUSE Build Service repository] (http://download.opensuse.org/repositories/home:/flixr:/paparazzi-uav/Debian_7.0/)
Debian/Ubuntu packages:
- **paparazzi-dev** is the meta-package on which the Paparazzi software depends to compile and run the ground segment and simulator.
- **paparazzi-jsbsim** is needed for using JSBSim as flight dynamics model for the simulator.
Recommended cross compiling toolchain: https://launchpad.net/gcc-arm-embedded
Directories quick and dirty description:
To run the verification, the following software are required:
- Frama-C, the compiled version from the
[source](https://git.frama-c.com/pub/frama-c), tested on commit:
3fa7de0c695188a9b0adf7a8b8bfb24a335c1df7
- Alt-Ergo 2.3.3
- CVC4 1.9-prerelease
- Z3 4.8.6
- ctags
How to run the verification:
-------------
```
cd sw/airborne
```
Update the variable `FRAMAC_PREFIX` in `frama-c-analysis.sh`
with the path of the directory containing Frama-C binary. Then,
launch the script that start the analysis:
```
./frama-c-analysis.sh
```
Quick descritpion of modified files:
----------------------------------------
_conf_: the configuration directory (airframe, radio, ... descriptions).
_data_: where to put read-only data (e.g. maps, terrain elevation files, icons)
_doc_: documentation (diagrams, manual source files, ...)
_sw_: software (onboard, ground station, simulation, ...)
_var_: products of compilation, cache for the map tiles, ...
Compilation and demo simulation
-------------------------------
1. type "make" in the top directory to compile all the libraries and tools.
2. "./paparazzi" to run the Paparazzi Center
3. Select the "Microjet" aircraft in the upper-left A/C combo box.
Select "sim" from upper-middle "target" combo box. Click "Build".
When the compilation is finished, select "Simulation" from
the upper-right session combo box and click "Execute".
4. In the GCS, wait about 10s for the aircraft to be in the "Holding point" navigation block.
Switch to the "Takeoff" block (lower-left blue airway button in the strip).
Takeoff with the green launch button.
Uploading the embedded software
----------------------------------
1. Power the flight controller board while it is connected to the PC with the USB cable.
2. From the Paparazzi center, select the "ap" target, and click "Upload".
Flight
------
1. From the Paparazzi Center, select the flight session and ... do the same as in simulation !
- `sw/airborne/frama-c-analysis.sh`: Script to automatically
launch the verification using Frama-C.
- `sw/airborne/output-frama-c-analysis.sh`: A python script
used by `frama-c-analysis.sh` to read and analyse the results
from Frama-C.
- `sw/airborne/math/pprz_algebra_(int|float|double).(h|c)`:
Mathematical library of Paparazzi that has been verified. These
files have been annotated with ACSL.
- `sw/airborne/math/pprz_algebra_(int|float|double)_frama_c.h`:
Files containing definition of predicates, lemma and logical
functions used to verify the absence of RTE in the library.
- `sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h`:
Definition of predicates, lemma and logical functions for the
verification of functional properties.
The verification:
-------------
The Frama-C verification combines the analysis of the [EVA]
(https://frama-c.com/fc-plugins/eva.html) and
[WP](https://frama-c.com/fc-plugins/wp.html) plugins. The
plugin EVA requires a program entry point (a
main or a function) to start its analysis. The script
`frama-c-analysis.sh` find automatically all the function's
name of the library using ctags. Then, the verification is
launched for every function.
When Frama-C is launched, the C constant `FRAMA_C_ANALYSIS` is
defined in order to remove certain portions of code that are not
supported by Frama-C.
More information about Paparazzi
--------------------------------
To have information about Paparazzi, go directly on the
[website](https://wiki.paparazziuav.org/wiki/Main_Page) or on
the [GitLab project](https://github.com/paparazzi/paparazzi).
\ No newline at end of file
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @ 1e2d688a
......@@ -56,10 +56,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 6,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_2 rm_0)",
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -68,10 +68,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 6,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -80,10 +80,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 4,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @ 1e2d688a
......@@ -56,10 +56,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 6,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_2 rm_0)",
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -68,10 +68,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 6,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -80,10 +80,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 4,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @ 1e2d688a
......@@ -17,10 +17,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 6,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_2 rm_0)",
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -29,10 +29,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 6,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -86,20 +86,20 @@
{ "Goal 1/4":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.7552,
"steps": 357 } ],
"time": 4.0255,
"steps": 752 } ],
"Goal 2/4":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.3541,
"steps": 380 } ],
"time": 4.6182,
"steps": 779 } ],
"Goal 3/4":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.2624,
"steps": 379 } ],
"time": 4.7327,
"steps": 778 } ],
"Goal 4/4":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.2096,
"steps": 379 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 3.5847,
"steps": 778 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @ 1e2d688a
......@@ -66,10 +66,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 6,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_2 rm_0)",
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -78,10 +78,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 6,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -90,14 +90,14 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 4,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 4.7685,
"steps": 1358 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 4.3424,
"steps": 2277 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert.json
View file @ 1e2d688a
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.67 } ],
"verdict": "valid", "time": 0.73 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.1 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.74 } ],
"verdict": "valid", "time": 4.36 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_2.json
View file @ 1e2d688a
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.04 } ],
"verdict": "valid", "time": 2.81 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.67 } ],
"verdict": "valid", "time": 4.6 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.18 } ],
"verdict": "valid", "time": 3.75 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_3.json
View file @ 1e2d688a
......@@ -3,8 +3,8 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "time": 0.06,
"steps": 147830 } ],
"verdict": "valid", "time": 0.07,
"steps": 147844 } ],
"OnLeft": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step",
......@@ -15,7 +15,7 @@
"children": { "Unfold 'P_unary_quaterion'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.86 } ] } } ],
"time": 5.56 } ] } } ],
"OnRight": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step",
......@@ -26,5 +26,5 @@
"children": { "Unfold 'P_unary_quaterion'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 4.5 } ] } } ],
"time": 6.2 } ] } } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_4.json
View file @ 1e2d688a
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.96 } ],
"verdict": "valid", "time": 4.77 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 10.06 } ],
"verdict": "valid", "time": 9.32 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 8.87 } ],
"verdict": "valid", "time": 9.83 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures.json
View file @ 1e2d688a
......@@ -31,7 +31,7 @@
{ "Unfold 'L_l_RMat_of_FloatQuat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 7.45 } ] } } ] } } ],
"time": 7.99 } ] } } ] } } ],
"Goal 2/9":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -65,7 +65,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.1 } ] } } ] } } ] } } ],
"time": 0.15 } ] } } ] } } ] } } ],
"Goal 3/9":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -99,7 +99,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.12 } ] } } ] } } ] } } ],
"time": 0.1 } ] } } ] } } ] } } ],
"Goal 4/9":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -133,7 +133,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.1 } ] } } ] } } ] } } ],
"time": 0.09 } ] } } ] } } ] } } ],
"Goal 5/9":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -147,7 +147,7 @@
{ "Unfold 'L_transpose'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 11.7041,
"time": 13.2174,
"steps": 114 } ] } } ],
"Goal 6/9":
[ { "header": "Definition",
......@@ -206,7 +206,7 @@
{ "Unfold 'L_l_RMat_of_FloatQuat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 15.2679,
"time": 17.259,
"steps": 114 } ] } } ] } } ],
"Goal 8/9":
[ { "header": "Definition",
......@@ -221,10 +221,10 @@
{ "Unfold 'L_transpose'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 13.6175,
"time": 12.9716,
"steps": 114 } ] } } ],
"Goal 9/9":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 9.1711,
"time": 8.7372,
"steps": 114 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
View file @ 1e2d688a
......@@ -98,7 +98,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.8506,
"time": 3.8436,
"steps": 12 } ] } } ] } } ],
"Goal 3/9":
[ { "header": "Definition",
......@@ -113,7 +113,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 8.6803,
"time": 10.1864,
"steps": 122 } ] } } ],
"Goal 4/9":
[ { "header": "Definition",
......@@ -140,7 +140,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 4.8108,
"time": 3.5714,
"steps": 12 } ] } } ] } } ],
"Goal 5/9":
[ { "header": "Definition",
......@@ -165,7 +165,7 @@
{ "Unfold 'L_id_rmat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 6.6462,
"time": 6.547,
"steps": 118 } ] } } ] } } ],
"Goal 6/9":
[ { "header": "Definition",
......@@ -180,7 +180,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 8.5869,
"time": 10.2964,
"steps": 122 } ] } } ],
"Goal 7/9":
[ { "header": "Definition",
......@@ -195,7 +195,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 7.8722,
"time": 11.272,
"steps": 122 } ] } } ],
"Goal 8/9":
[ { "header": "Definition",
......@@ -210,7 +210,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 8.5394,
"time": 9.7008,
"steps": 122 } ] } } ],
"Goal 9/9":
[ { "header": "Definition",
......@@ -225,5 +225,5 @@
{ "Unfold 'L_id_rmat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 12.069,
"time": 11.9225,
"steps": 116 } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_5.json
View file @ 1e2d688a
......@@ -2,6 +2,12 @@
"select": { "select": "clause-step", "at": 31, "kind": "have",
"target": "let a_1 = Mptr_0[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_0 Mptr_0\n (havoc Mint_undef_0 Mint_9 (shift_sint32 a_1 0) l_3)[(shift_sint32 a_1 j_0)\n ->v_0] a_0 m_2 n_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 10. },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.47 } ] } } ]
"time": 7.28 },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. } ] } } ]
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_6.json
View file @ 1e2d688a
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step", "at": 30, "kind": "have",
"target": "let a_0 = Mptr_0[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_0 Mptr_0\n (havoc Mint_undef_0 Mint_9 (shift_sint32 a_0 0) l_3)[(shift_sint32 a_0 j_0)\n ->v_0] b_0 n_0 l_3\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"select": { "select": "clause-step", "at": 31, "kind": "have",
"target": "let a_1 = Mptr_0[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_0 Mptr_0\n (havoc Mint_undef_0 Mint_9 (shift_sint32 a_1 0) l_3)[(shift_sint32 a_1 j_0)\n ->v_0] a_0 m_2 n_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.66 } ] } } ]
"time": 0.87,
"steps": 2170940 },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. } ] } } ]
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_7.json
View file @ 1e2d688a
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},