package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/src/frama-c-e-acsl.core/e_ACSL.ml.html

Source file `e_ACSL.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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
(* generated by dune *)

(** @canonical E_ACSL.Analyses *)
module Analyses = E_ACSL__Analyses

(** @canonical E_ACSL.Analyses_datatype *)
module Analyses_datatype = E_ACSL__Analyses_datatype

(** @canonical E_ACSL.Analyses_types *)
module Analyses_types = E_ACSL__Analyses_types

(** @canonical E_ACSL.Assert *)
module Assert = E_ACSL__Assert

(** @canonical E_ACSL.Assigns *)
module Assigns = E_ACSL__Assigns

(** @canonical E_ACSL.Bound_variables *)
module Bound_variables = E_ACSL__Bound_variables

(** @canonical E_ACSL.Builtins *)
module Builtins = E_ACSL__Builtins

(** @canonical E_ACSL.Contract *)
module Contract = E_ACSL__Contract

(** @canonical E_ACSL.Contract_types *)
module Contract_types = E_ACSL__Contract_types

(** @canonical E_ACSL.E_acsl_visitor *)
module E_acsl_visitor = E_ACSL__E_acsl_visitor

(** @canonical E_ACSL.Env *)
module Env = E_ACSL__Env

(** @canonical E_ACSL.Error *)
module Error = E_ACSL__Error

(** @canonical E_ACSL.Exit_points *)
module Exit_points = E_ACSL__Exit_points

(** @canonical E_ACSL.Functions *)
module Functions = E_ACSL__Functions

(** @canonical E_ACSL.Global_observer *)
module Global_observer = E_ACSL__Global_observer

(** @canonical E_ACSL.Gmp *)
module Gmp = E_ACSL__Gmp

(** @canonical E_ACSL.Gmp_types *)
module Gmp_types = E_ACSL__Gmp_types

(** @canonical E_ACSL.Injector *)
module Injector = E_ACSL__Injector

(** @canonical E_ACSL.Interval *)
module Interval = E_ACSL__Interval

(** @canonical E_ACSL.Interval_utils *)
module Interval_utils = E_ACSL__Interval_utils

(** @canonical E_ACSL.Labels *)
module Labels = E_ACSL__Labels

(** @canonical E_ACSL.Libc *)
module Libc = E_ACSL__Libc

(** @canonical E_ACSL.Literal_observer *)
module Literal_observer = E_ACSL__Literal_observer

(** @canonical E_ACSL.Literal_strings *)
module Literal_strings = E_ACSL__Literal_strings

(** @canonical E_ACSL.Logic_aggr *)
module Logic_aggr = E_ACSL__Logic_aggr

(** @canonical E_ACSL.Logic_array *)
module Logic_array = E_ACSL__Logic_array

(** @canonical E_ACSL.Logic_functions *)
module Logic_functions = E_ACSL__Logic_functions

(** @canonical E_ACSL.Logic_normalizer *)
module Logic_normalizer = E_ACSL__Logic_normalizer

(** @canonical E_ACSL.Loops *)
module Loops = E_ACSL__Loops

(** @canonical E_ACSL.Lscope *)
module Lscope = E_ACSL__Lscope

(** @canonical E_ACSL.Main *)
module Main = E_ACSL__Main

(** @canonical E_ACSL.Memory_observer *)
module Memory_observer = E_ACSL__Memory_observer

(** @canonical E_ACSL.Memory_tracking *)
module Memory_tracking = E_ACSL__Memory_tracking

(** @canonical E_ACSL.Memory_translate *)
module Memory_translate = E_ACSL__Memory_translate

(** @canonical E_ACSL.Misc *)
module Misc = E_ACSL__Misc

(** @canonical E_ACSL.Options *)
module Options = E_ACSL__Options

(** @canonical E_ACSL.Prepare_ast *)
module Prepare_ast = E_ACSL__Prepare_ast

(** @canonical E_ACSL.Quantif *)
module Quantif = E_ACSL__Quantif

(** @canonical E_ACSL.Rte *)
module Rte = E_ACSL__Rte

(** @canonical E_ACSL.Rtl *)
module Rtl = E_ACSL__Rtl

(** @canonical E_ACSL.Smart_exp *)
module Smart_exp = E_ACSL__Smart_exp

(** @canonical E_ACSL.Smart_stmt *)
module Smart_stmt = E_ACSL__Smart_stmt

(** @canonical E_ACSL.Temporal *)
module Temporal = E_ACSL__Temporal

(** @canonical E_ACSL.Translate_annots *)
module Translate_annots = E_ACSL__Translate_annots

(** @canonical E_ACSL.Translate_ats *)
module Translate_ats = E_ACSL__Translate_ats

(** @canonical E_ACSL.Translate_predicates *)
module Translate_predicates = E_ACSL__Translate_predicates

(** @canonical E_ACSL.Translate_rtes *)
module Translate_rtes = E_ACSL__Translate_rtes

(** @canonical E_ACSL.Translate_terms *)
module Translate_terms = E_ACSL__Translate_terms

(** @canonical E_ACSL.Translate_utils *)
module Translate_utils = E_ACSL__Translate_utils

(** @canonical E_ACSL.Translation_error *)
module Translation_error = E_ACSL__Translation_error

(** @canonical E_ACSL.Typed_number *)
module Typed_number = E_ACSL__Typed_number

(** @canonical E_ACSL.Typing *)
module Typing = E_ACSL__Typing

(** @canonical E_ACSL.Varname *)
module Varname = E_ACSL__Varname

(** @canonical E_ACSL.Widening *)
module Widening = E_ACSL__Widening