Module `Program.Domain`

Domain identification

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

include sig ... end

val id : unit Mopsa_analyzer__Framework__Core__Id.id

val name : string

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

Command line options

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

val opt_entry_function : string ref

Name of the entry function to be analyzed.

val opt_check_memory : bool ref

val opt_symbolic_args : (int * int option) option ref

Symbolic main arguments.

val parse_symbolic_args_spec : string -> int * int option

val opt_arg_max_size : int option ref

val opt_arg_min_size : int option ref

val checks : 'a list

Initialization of environments

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

val init : 
  MopsaLib.program ->
  'a ->
  'b Mopsa_analyzer.MopsaLib.Flow.flow ->
  'b Mopsa_analyzer.MopsaLib.Post.post option

Computation of post-conditions

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

val init_globals : 
  (MopsaLib.var * Lang.Ast.c_var_init option) list ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  'a Mopsa_analyzer.MopsaLib.Post.post

Initialize global variables

val exec_stub_directives : 
  Stubs.Ast.stub_directive list ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  'a Mopsa_analyzer.MopsaLib.Post.post

Execute stub directives

val find_function : string -> Lang.Ast.c_fundec list -> Lang.Ast.c_fundec

Fund a function by name

val find_variable : string -> (MopsaLib.var * 'a) list -> MopsaLib.var

Find a global variable by name

val check_memory_allocation : 
  ('a, 'b) MopsaLib.man ->
  Mopsa_utils.Core.Location.range ->
  'a Core.Flow.flow ->
  'a Core.Flow.flow

val exec_exit_functions_with_loop : 
  Z.t ->
  Z.t ->
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, unit) Core.Cases.cases

Execute exit functions using a loop

val exec_exit_functions : 
  string ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow ->
  'a Mopsa_analyzer.MopsaLib.Post.post

Execute functions registered with atexit

val exec_entry_body : 
  Lang.Ast.c_fundec ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  'a Core.Post.post

Creation of argc and argv

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

val argv_resource : string

val arg_single_resource : int -> string

val arg_smash_resource : int -> string

val is_argv_resource : string -> bool

val is_arg_single_resource : string -> bool

val is_arg_smash_resource : string -> bool

val is_arg_resource : string -> bool

val alloc_argv : 
  MopsaLib.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, Framework.Core.Ast.Expr.expr) Mopsa_analyzer.MopsaLib.Cases.cases

Allocate the argv array

val alloc_concrete_arg : 
  int ->
  MopsaLib.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, Framework.Core.Ast.Expr.expr) Mopsa_analyzer.MopsaLib.Cases.cases

Allocate an address for a concrete argument

val init_concrete_arg : 
  MopsaLib.expr ->
  string ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  'a Core.Post.post

Initialize an argument with a concrete string

val eval_bytes : 
  MopsaLib.expr ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  'a Framework.Core.Eval.eval

val call_main_with_concrete_args : 
  Lang.Ast.c_fundec ->
  string list ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, unit) Mopsa_analyzer.MopsaLib.Cases.cases

Initialize argc and argv with concrete values and execute the body of main

val alloc_symbolic_args : 
  int ->
  int ->
  MopsaLib.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, Framework.Core.Ast.Expr.expr list * Framework.Core.Ast.Expr.expr option)
    Mopsa_analyzer.MopsaLib.Cases.cases

Allocate addresses for symbolic arguments

val assume_valid_string : 
  MopsaLib.expr ->
  Framework.Core.Ast.Var.var ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, unit) Mopsa_analyzer.MopsaLib.Cases.cases

val memset_argv_with_smash : 
  MopsaLib.expr ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  int ->
  Framework.Core.Ast.Var.var ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  'a Mopsa_analyzer.MopsaLib.Post.post

val call_main_with_symbolic_args : 
  Lang.Ast.c_fundec ->
  int ->
  int option ->
  ('a, 'b) MopsaLib.man ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow ->
  ('a, unit) Core.Cases.cases

Initialize argc and argv with symbolic arguments

val call_main : 
  Lang.Ast.c_fundec ->
  string list option ->
  'a ->
  ('b, 'c) MopsaLib.man ->
  'b Core.Flow.flow ->
  ('b, unit) Core.Cases.cases

val exec : 
  MopsaLib.stmt ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, unit) Core.Cases.cases option

Evaluation of expressions

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

val eval_exit : 
  string ->
  Framework.Core.Ast.Expr.expr ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, Framework.Core.Ast.Expr.expr) Mopsa_analyzer.MopsaLib.Cases.cases

val eval : 
  MopsaLib.expr ->
  ('a, 'b) MopsaLib.man ->
  'a Core.Flow.flow ->
  ('a, Framework.Core.Ast.Expr.expr) Mopsa_analyzer.MopsaLib.Cases.cases option

Handler of queries

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

val ask : 
  'r. ('a, 'r) MopsaLib.query ->
  ('a, 'b) MopsaLib.man ->
  'a MopsaLib.flow ->
  ('a, 'r) MopsaLib.cases option

val print_expr : 'a -> 'b -> 'c -> 'd -> unit

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Iterators/Program/Domain/index.html

Module `Program.Domain`

Creation of argc and argv

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Iterators/Program/Domain/index.html

Module Program.Domain

Creation of argc and argv

dune-project
Dependency

Module `Program.Domain`