package frama-c-rpp

  1. Overview
  2. Docs
RPP plugin of Frama-C for writing and proving relational properties

Install 

dune-project
 Dependency

frama-c.com Readme Edit opam file Versions (1)

Authors

  1. L
    Lionel Blatter

Maintainers

  1. V
    virgile.prevosto@cea.fr

Sources

v0.0.4.tar.gz
md5=c1f95410aaa8839ae6b9c3e4dc13259a
sha512=c999f46044866a492c8649cd68cb37b0f0ee90f1126ec5395df7ffcfbf6e0e52bc8c344d14c6f6fba17fca6c0ae1f27bf48fc4bc20ccfeaacf987c7376b7d203

doc/frama-c-rpp.core/Rpp/class-generation_of_proof_system/index.html

Class Rpp.generation_of_proof_systemSource

inherit Frama_c_kernel.Visitor.generic_frama_c_visitor
method add_new_global : Frama_c_kernel.Cil_types.global -> unit