TrustInSoft Documentation
1.43.3-1414-g15aca82742
Sections
Tutorials
User Manual
Reference Manual
Coding Standards
Glossary
Useful Links
Changelog
New Functionalities
« User Manual
Introduction »
Search
Tutorials
User Manual
TrustInSoft Analyzer Manual
Introduction
Prepare the Sources
Prepare the Analysis
Get the Information
Study the Alarms
ACSL Properties
Prove Annotations with WP
Conclusion
Analyzing C++ Programs
Dealing with Special Features
Verification of properties set at the design stage
TrustInSoft Analyzer GUI Manual
tis-aggregate Manual
tis-info Manual
tis-mk-main Manual
tis-mkfs Manual
tis-modifications Manual
tis-fuzz Manual
tis-report Manual
Reference Manual
Coding Standards
Glossary
Useful Links
Changelog
New Functionalities
TrustInSoft Analyzer Manual
ΒΆ
Introduction
Prepare the Sources
Prepare the Analysis
Get the Information
Study the Alarms
ACSL Properties
Prove Annotations with WP
Conclusion
Analyzing C++ Programs
TrustInSoft Analyzer++ Specificities
Identifiers
Mangling
Demangling
Mangling-related options
Functions and methods
Argument passing
Scalar types
Reference types
Class types
Unknown passing style
Method transformations
Constructor elision
Virtual method calls
Controlling the virtual method calls translation
Objects memory layout
Empty classes
Non-virtual inheritance
Polymorphic classes
Virtual inheritance
Layout summary
Member pointers
Pointers to member functions declaration
Program initialization
Dynamic initialization
Static initialization
Static local variables
Special variable names
Global variables
Intermediate variables
Generated contracts
GoogleTest support
Options
Configuration
Running the analysis
Limitations
Dealing with Special Features
File System
Environment variables
Setting environment variables
Initializing the whole environment
Using the environment
Advanced usage
Recursive calls
Memory leaks
Target Architecture
New Architecture on the Fly
Additional target architecture tuning for floating-point behavior
Additional tuning for the typing of integer constants
Assembler Code
Physical Addresses
Valid memory accesses
With the option
With code modification
Constraints on physical addresses
Physical addresses of global variables
Alignment
Set address bits
Dynamic loading
Compiler Specific Keywords
Multi-Threading
Strict Aliasing
The analysis
Strict Aliasing Analysis Options
The option
-sa-strict-enum
The option
-sa-strict-struct
The option
-sa-strict-union
Volatile Variables
The option
-volatile-globals
Functions With Variable Arguments
The
C11
standard references
Limitations: what is not satisfying the standard?
The
va_list
type
Only in local variables
Assignments
Casting
Casts to the
va_list
type
Casts from the
va_list
type
Passing
va_list
objects to other functions
Returning
va_list
objects from functions
Undefined behavior cases not completely verified
Invoking
va_arg
on
va_list
objects passed to other functions
Suppressing definitions of variadic macros
The type parameter of the
va_arg
macro
The
parmN
parameter of the
va_arg
macro
Old-style variadic macros
Functions from <math.h>
Floating-point
Data Representation
Building an abstract float
Choosing the dialect for the analyzed program
Option enum-restriction
Option -pointer-arguments-to-std-functions
Deterministic libc
Endianness
Random
Time
Verification of properties set at the design stage