package mopsa

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Command-line options
Contexts
Entry point
functions
Scope update
Statements
Expressions
Variables
Types
Ranges and locations
Stubs annotations

MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install

dune-project

Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

Maintainers

Sources

mopsa-analyzer-v1.2.tar.gz

md5=37966e98ffeebcedc09bd6e9b2b81f69

sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Lang/Frontend/index.html

Module `Lang.Frontend`

C front-end to translate parser AST into MOPSA AST

val debug : ('a, Format.formatter, unit, unit) format4 -> 'a

Command-line options

========================

val opt_clang : string list ref

Extra options to pass to clang when parsing

val opt_include_dirs : string list ref

List of include directories

val opt_make_target : string ref

Name of the target binary to analyze

val opt_without_libc : bool ref

Disable stubs of the standard library

val opt_enable_cache : bool ref

Enable the parser cache.

val opt_warn_all : bool ref

Display all compiler warnings

val opt_use_stub : string list ref

Lists of functions that the body will be replaced by a stub

val opt_library_only : bool ref

Allow library-only targets in the .db files (used for multilanguage analysis)

val opt_target_triple : string ref

Target architecture triple to analyze for (host if left empty)

val opt_stubs_files : string list ref

Additional stub files to parse

val opt_ignored_translation_units : String.t list ref

List of translation units to ignore during linking

val opt_save_preprocessed_file : string ref

Where to save the preprocessed file

val opt_store_project : bool ref

Store project in memory for automated testcase reduction capabilities

Contexts

============

type type_space =

| TS_TYPEDEF
| TS_RECORD
| TS_ENUM

type ctx = {

ctx_prj : Mopsa_c_parser.C_AST.project;
ctx_fun : Lang.Ast.c_fundec Mopsa_c_parser.C_AST.StringMap.t;
ctx_type : (type_space * string, MopsaLib.typ) Hashtbl.t;
ctx_vars : (int * string, MopsaLib.var * Mopsa_c_parser.C_AST.variable) Hashtbl.t;
ctx_macros : Mopsa_c_parser.C_AST.macro Mopsa_c_parser.C_AST.StringMap.t;
ctx_predicates : Mopsa_c_stubs_parser.Passes.Preprocessor.predicate Mopsa_c_parser.C_AST.StringMap.t;
ctx_stubs : (string, Mopsa_c_stubs_parser.Cst.stub) Hashtbl.t;
ctx_enums : Z.t Mopsa_c_parser.C_AST.StringMap.t;

}

val input_files : string list ref

List of input files

val target_info : Mopsa_c_parser.Clang_AST.target_info ref

Target information used for parsing

val o_prj : Mopsa_c_parser.C_AST.project option ref

Saved project

val find_function_in_context : 
  ctx ->
  Mopsa_utils.Core.Location.range ->
  Mopsa_c_parser.C_AST.func ->
  Lang.Ast.c_fundec

val get_parsed_system_headers : 
  Mopsa_c_parser.Clang_to_C.context ->
  string list

val get_all_stubs : unit -> string list

val find_stubs_of_header : string -> string list -> string list

val is_ignored_translation_unit : string -> bool

val save_preprocessed_file : 
  Mopsa_c_parser.C_AST.project ->
  string ->
  string list

Entry point

===============

val parse_program : string list -> MopsaLib.program

val parse_db : string -> Mopsa_c_parser.Clang_to_C.context -> unit

val parse_file : 
  string ->
  ?nb:(int * int) ->
  ?stub:bool ->
  string list ->
  string ->
  bool ->
  bool ->
  Mopsa_c_parser.Clang_to_C.context ->
  unit

val parse_stubs : Mopsa_c_parser.Clang_to_C.context -> unit -> unit

val from_project : Mopsa_c_parser.C_AST.project -> MopsaLib.prog_kind

val find_target : String.t -> string list -> string

functions

=============

val from_function : Mopsa_c_parser.C_AST.func -> Lang.Ast.c_fundec

Scope update

****************

val from_scope_update : 
  ctx ->
  Mopsa_c_parser.C_AST.scope_update ->
  Lang.Ast.c_scope_update

Statements

==============

val from_stmt : ctx -> Mopsa_c_parser.C_AST.statement -> MopsaLib.stmt

val from_block : 
  ctx ->
  MopsaLib.range ->
  Mopsa_c_parser.C_AST.block ->
  MopsaLib.stmt

val from_body_option : 
  ctx ->
  MopsaLib.range ->
  Mopsa_c_parser.C_AST.block option ->
  MopsaLib.stmt option

Expressions

===============

val from_expr : ctx -> Mopsa_c_parser.C_AST.expr -> MopsaLib.expr

val from_expr_option : 
  ctx ->
  Mopsa_c_parser.C_AST.expr option ->
  MopsaLib.expr option

val from_unary_operator : 
  Mopsa_c_parser.C_AST.unary_operator ->
  MopsaLib.typ ->
  Framework.Core.Ast.Operator.operator

val from_binary_operator : 
  Mopsa_c_parser.C_AST.binary_operator ->
  MopsaLib.typ ->
  Framework.Core.Ast.Operator.operator

val from_character_kind : 
  Mopsa_c_parser.C_AST.character_kind ->
  Lang.Ast.c_character_kind

Variables

=============

val from_var : ctx -> Mopsa_c_parser.C_AST.variable -> MopsaLib.var

val patch_array_parameters : MopsaLib.var -> MopsaLib.var

val from_var_scope : 
  ctx ->
  Mopsa_c_parser.C_AST.variable_kind ->
  Lang.Ast.c_var_scope

val from_var_init : 
  ctx ->
  Mopsa_c_parser.C_AST.variable ->
  Lang.Ast.c_var_init option

val from_init_option : 
  ctx ->
  Mopsa_c_parser.C_AST.init option ->
  Lang.Ast.c_var_init option

val from_init : ctx -> Mopsa_c_parser.C_AST.init -> Lang.Ast.c_var_init

Types

=========

val from_typ : ctx -> Mopsa_c_parser.C_AST.type_qual -> MopsaLib.typ

val from_unqual_typ : ctx -> Mopsa_c_parser.C_AST.typ -> MopsaLib.typ

val from_integer_type : 
  Mopsa_c_parser.C_AST.integer_type ->
  Lang.Ast.c_integer_type

val from_float_type : Mopsa_c_parser.C_AST.float_type -> Lang.Ast.c_float_type

val from_array_length : 
  ctx ->
  Mopsa_c_parser.C_AST.array_length ->
  Lang.Ast.c_array_length

val from_function_type : 
  ctx ->
  Mopsa_c_parser.C_AST.function_type ->
  Lang.Ast.c_function_type

val find_field_index : Mopsa_c_parser.C_AST.type_qual -> string -> int

val under_type : 
  Mopsa_c_parser.C_AST.type_qual ->
  Mopsa_c_parser.C_AST.type_qual

Ranges and locations

========================

val from_loc : Mopsa_c_parser.Clang_AST.loc -> Mopsa_utils.Core.Location.pos

val from_eloc : Mopsa_c_parser.Clang_AST.eloc -> Mopsa_utils.Core.Location.epos

val from_range : Mopsa_c_parser.C_AST.range -> MopsaLib.range

Stubs annotations

=====================

val from_stub_comment : 
  ctx ->
  Mopsa_c_parser.C_AST.func ->
  Stubs.Ast.stub_func option

val from_stub_func : 
  ctx ->
  Mopsa_c_parser.C_AST.func ->
  Parsing.Ast.stub ->
  Stubs.Ast.stub_func

val from_stub_section : ctx -> Parsing.Ast.section -> Stubs.Ast.section

val from_stub_leaf : ctx -> Parsing.Ast.leaf -> Stubs.Ast.leaf

val from_stub_case : ctx -> Parsing.Ast.case -> Stubs.Ast.case

val from_stub_requires : 
  ctx ->
  Parsing.Ast.requires Mopsa_utils.Core.Location.with_range ->
  Stubs.Ast.requires MopsaLib.with_range

val from_stub_free : 
  ctx ->
  Parsing.Ast.free Mopsa_utils.Core.Location.with_range ->
  Stubs.Ast.free MopsaLib.with_range

val from_stub_message : 
  ctx ->
  Parsing.Ast.message Mopsa_utils.Core.Location.with_range ->
  Stubs.Ast.message MopsaLib.with_range

val from_stub_message_kind : Parsing.Ast.message_kind -> Stubs.Ast.message_kind

val from_stub_assigns : 
  ctx ->
  Parsing.Ast.assigns Mopsa_utils.Core.Location.with_range ->
  Stubs.Ast.assigns MopsaLib.with_range

val from_stub_local : 
  ctx ->
  Parsing.Ast.local Mopsa_utils.Core.Location.with_range ->
  Stubs.Ast.local MopsaLib.with_range

val from_stub_local_value : 
  ctx ->
  Parsing.Ast.local_value ->
  Stubs.Ast.local_value

val from_stub_ensures : 
  ctx ->
  Parsing.Ast.ensures Mopsa_utils.Core.Location.with_range ->
  Stubs.Ast.ensures MopsaLib.with_range

val from_stub_assumes : 
  ctx ->
  Parsing.Ast.assumes Mopsa_utils.Core.Location.with_range ->
  Stubs.Ast.assumes MopsaLib.with_range

val from_stub_formula : ctx -> Parsing.Ast.requires -> Stubs.Ast.requires

val from_stub_set : ctx -> Parsing.Ast.set -> Stubs.Ast.set

val from_stub_interval : ctx -> Parsing.Ast.interval -> Stubs.Ast.interval

val from_stub_expr : ctx -> Parsing.Ast.free -> Stubs.Ast.free

val from_stub_log_binop : Parsing.Ast.log_binop -> Stubs.Ast.log_binop

val from_stub_expr_binop : 
  Mopsa_c_stubs_parser.Ast.binop ->
  Framework.Core.Ast.Operator.operator

val from_stub_expr_unop : 
  Mopsa_c_stubs_parser.Ast.unop ->
  Framework.Core.Ast.Operator.operator

val from_stub_directives : 
  ctx ->
  (Mopsa_c_parser.Clang_AST.comment
   * Mopsa_c_parser.C_AST.macro Mopsa_c_parser.C_AST.StringMap.t)
    list
    Mopsa_c_parser.C_AST.RangeMap.t ->
  Stubs.Ast.stub_directive list

val from_stub_directive : ctx -> Parsing.Ast.stub -> Stubs.Ast.stub_directive

val from_stub_predicates : 
  (Mopsa_c_parser.Clang_AST.comment
   * Mopsa_c_parser.Clang_AST.macro Mopsa_c_parser.C_AST.StringMap.t)
    list
    Mopsa_c_parser.C_AST.RangeMap.t ->
  Mopsa_c_stubs_parser.Passes.Preprocessor.predicate
    Mopsa_c_parser.C_AST.StringMap.t

val on_panic : exn -> string list -> float -> unit