SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:external_plugins [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools


mantis:frama-c:external_plugins

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
mantis:frama-c:external_plugins [2013/03/12 17:22]
ploc
mantis:frama-c:external_plugins [2013/05/31 13:06]
djs52
Line 17: Line 17:
 ===== Celia ===== ===== Celia =====
  
-URL: http://​www.liafa.jussieu.fr/celia+URL: http://​www.liafa.univ-paris-diderot.fr/celia/
  
 CELIA is a tool for the static analysis and verification of C programs manipulating dynamic (singly linked) lists. The static analyser computes for each control point of a C program the assertions which are true (i.e., invariant) at this control point. These asssertions express properties about the shape of the lists, their size, the relations between the data (or the sum, or the multiset of data) in list cells. The analysis is inter-procedural,​ i.e., the assertions computed relate the procedure local heap on entry to the corresponding local heap on exit of the procedure. The results of the analysis can provide insights about equivalence of procedures on lists or null pointer dereferencing. The verifier is an experimental feature. ​ CELIA is a tool for the static analysis and verification of C programs manipulating dynamic (singly linked) lists. The static analyser computes for each control point of a C program the assertions which are true (i.e., invariant) at this control point. These asssertions express properties about the shape of the lists, their size, the relations between the data (or the sum, or the multiset of data) in list cells. The analysis is inter-procedural,​ i.e., the assertions computed relate the procedure local heap on entry to the corresponding local heap on exit of the procedure. The results of the analysis can provide insights about equivalence of procedures on lists or null pointer dereferencing. The verifier is an experimental feature. ​
Line 43: Line 43:
 It provides a grammar extension of specification allowing to specify the target tactic. It provides a grammar extension of specification allowing to specify the target tactic.
  
 +===== Simple Concurrency =====
  
 +URL: https://​bitbucket.org/​adelard/​simple-concurrency/​
 +
 +This plugin, developed by [[http://​www.adelard.com|Adelard]],​ provides a simple way to discover potential concurrency problems in interrupt-driven C code, and is intended for use with small embedded systems. It operates without using the value analysis plugin, which makes it fast but unable to analyse pointers. Command-line and GUI versions are available.
mantis/frama-c/external_plugins.txt ยท Last modified: 2013/05/31 13:06 by djs52