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/src/frama-c-rpp.core/rpp_options.ml.html

Source file rpp_options.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

module Self = Plugin.Register(struct
    let name = "RPP"
    let shortname = "rpp"
    let help = "Prove relationel properties"
  end)

module Enabled = Self.False(struct
    let option_name = "-rpp"
    let help = "when on (off by default), prove relationnel properties and generate the corresponding logical definition."
  end)

module Enable_only_hyp = Self.False(struct
    let option_name = "-rpp-hyp"
    let help = "when on (off by default), only generate the logical definition of the relational proprerties."
  end)

module Enable_only_prove = Self.False(struct
    let option_name = "-rpp-pro"
    let help = "when on (off by default), only generate the code transformation for relational proprerties proof."
  end)

module Counting_relational_verification_function = State_builder.Counter
    (struct
      let name = "Count_relational_verify_function"
    end)

let emitter =
  Emitter.create "Rpp" [Emitter.Code_annot;Emitter.Funspec;Emitter.Global_annot;Emitter.Property_status]
    ~correctness:[] ~tuning: []

module Counting_local_variable_verification_function = State_builder.Counter
    (struct
      let name = "Counting_local_variable_verification_function"
    end)

module Counting_return_formals_verification_function = State_builder.Counter
    (struct
      let name = "Counting_return_formals_verification_function"
    end)

module Counting_return_formals_verification_function_axiom = State_builder.Counter
    (struct
      let name = "Counting_return_formals_verification_function_axiom"
    end)

module Counting_local_variable_copies = State_builder.Counter
    (struct
      let name = "Counting_local_variable_copies"
    end)

module Counting_axiome = State_builder.Counter
    (struct
      let name = "Counting_axiome"
    end)

module Counting_behavior = State_builder.Counter
    (struct
      let name = "Counting_behavior"
    end)

module Counting_label = State_builder.Counter
    (struct
      let name = "Counting_labes"
    end)

module Counting_aux_local_variable = State_builder.Counter
    (struct
      let name = "Counting_aux_local_variable"
    end)

module Is_buildin_rela_first =
  State_builder.Ref
    (Datatype.Bool)
    (struct
      let name = "Is_buildin_rela_first"
      let dependencies = []
      let default () = true
    end)