Known Issues

GUI

  • Some features are not “callstack wise” yet. Please report to the TrustInSoft support if you want a specific feature to be callstack wise. Features not supported yet:
    • Results and parameters of functions

In case of problems, which cannot be resolved by refreshing the browser’s page, the Clear cache and Reload button in the Options menu is available. This button will clear cached data and reload the browser’s page.

TrustInSoft Analyzer++

  • Unspecifed sequence detection has been currently disabled by default in C++, because it causes too many unwanted false positives.

Dev 1.42

TrustInSoft Analyzer

  • Add GNU specific error.h, in which error() is defined.
  • Add FreeBSD’s strnstr
  • Disallow the storage of addresses in enums.
  • Eliminate duplicated warnings during code translation.
  • Consider the case where a realloc call fails.
  • New option -strict-type-qualifier-merging strictly enforces type compatibility rules with respect to type qualifiers.
  • Functions with destructor attribute, as well as destructors of global C++ variables, will now get run at the end of the program’s entry point.
  • Add builtin “tis_init_type” that allows the initialization of memory blocks of a given type.
  • Support for the in keyword in ACSL
  • In accordance with the C standard (7.21.3.5), all open files are closed upon program termination.
  • Add builtin tis_show_recursively_each(void*) that prints the memory area at the given address and every memory area whose address is mentioned in what has already been printed.
  • Update the output representation of zero-sized memory allocation.
  • Improve analysis precision when weak base memory is introduced and also fix soundness when malloc is called in a non-unrolled loop with sizes that vary at each iteration.
  • Locations are now followed by an “(included from …)” message when applicable.
  • Consider realloc(…, 0) as undefined behavior.
  • Remove support for rarely useful origins of garble-mix values to optimize speed and memory of the Value analysis.
  • Fix crash when all the possible values for one of the operands are invalid.
  • Add deterministic isatty()
  • The value of the file position indicator after a successful call to ungetc() is now always undefined until all pushed-back characters are read back, conforming to C99/C11 J.1. The commonly encountered extension of decrementing the file position with each successful ungetc call, unless its value was zero before the call, which was the previous behavior, can be enabled by defining the __TIS_DEFINED_FILE_POSITION_INDICATOR preprocessor symbol.
  • The clone of the functions generated when using the -val-clone-on-recursive-calls options are now prefixed __tis_rec_ instead of __fc_clone_.
  • A new option, -cpp-target-option, causes a Clang-compatible -target'' argument to be passed to the preprocessor, when enabled. This ensures there are no host-platform-specific preprocessor symbols defined when preprocessing for a different machdep. The default preprocessor is now `clang -E, which accepts such an option. This option is set by default when using tis-analyzer, unless the`-cpp-tool’’ option is used.
  • Disallow linking distinct integer types, even when they have equal length and signedness.
  • Provide peak virtual memory usage information, when -time is set, to the -info-json-results and the standard output.
  • New -dead-xxx options to get information about dead code. Use -info-help to list them, or look at the documentation. The old -info-dead-blocks option is deprecated and replaced by -dead-bk-summary.
  • Improve tis-aggregate coverage HTML output, especially the statement coverage.
  • The -val-malloc-returns-null option is now set by default when using tis-kernel (no changes when tis-analyzer is used).
  • The -val-malloc-returns-null option is now disabled when setting the -val-profile interpreter option (no changes when tis-analyzer --interpreter is used). Note: the -val-malloc-returns-null can still be enabled if given on the command line after the -val-profile interpreter option.
  • The -val-malloc-returns-null option is now disabled when setting the -language-mode cxx option (no changes when tis-analyzer++ is used). Note: the -val-malloc-returns-null can still be enabled if given on the command line after the -language-mode cxx option.
  • New “Clone origin” column in the -info-functions result holding the name of the source function for the generated __tis_rec_ functions.
  • New “Starting line” and “Ending line” columns in the -info-functions result holding the line numbers of the function in its source file.
  • In the -info-json-result, some information available in program_points have been added or updated. See more about these changes in the section “User Manual > tis-info Manual > About Value analysis results > JSON format” of the user documentation.
  • New options for tis-aggregate coverage to either see or not the __tis_rec_ functions.
  • A ‘File’ column has been added to the tis-aggregate coverage results.
  • The default is now to print the dead statements list from tis-aggregate coverage to stdout, but the --output-file option can be used to put it in a file.
  • Fix the list of the dead statements generated by tis-aggregate coverage: some of them were not listed when some analyses did not include all the files.

TrustInSoft Analyzer++

  • Destructors will now be invoked for variable-length arrays of objects with nontrivial destructors.

GUI

  • A new entry “Track term [..]” has been added in the contextual menu on pointer expressions.

Release 1.41

TrustInSoft Analyzer

  • Provide deterministic implementations of time() and gettimeofday()
  • Enums that are defined in a function are now prefixed by the function name. This prevents some clashes among synonymous but unrelated local enums.
  • New option -pointer-arguments-to-std-functions to allow different kinds of enforcement for the validity of arguments to standard library functions, per C17 7.1.4:1.
  • Add builtin tis_id that returns a different number in each state it is called in and builtin tis_show_allocated_and_id that prints the value of its arguments in addition to a list of allocated blocks.
  • Transform the C99 minimal size hint on arrays in function parameters into a requires clause. (see 6.7.5.3p7 in C99).
  • Add command -machdep verbose to list the supported architectures with a brief summary of the main characteristics of each.
  • Support for __builtin_strlen() has been added.
  • Improve the information gained by the analyzer when encountering conditions such as “if (x % c1)” and “if (!(x % c1))”.
  • Add option enum-restriction (loose|strict|stricter) to allow to set the kinds of restriction for enumeration values.
  • Implement predicate inside_address_space that expresses the prerequisite on a pointer argument to a standard function, according to the option -pointer-arguments-to-std-functions.
  • Add interpreter support for POSIX endianness conversion functions
  • Improve the performance of the memcmp builtin with imprecise arguments.
  • Add interpreter support for standard C90 and POSIX random functions
  • Fix parsing of programs that contain GNU local labels declarations that used to be incorrectly rejected.
  • Added <syscall.h> header and many SYS_xxx values, to help parse code performing inline system call invocation.
  • Add support for inverse trigonometric function acos
  • Full support for the alias attribute on functions and variables.
  • Added <x86intrin.h>, <lzcntintrin.h> and <popcntintrin.h> non-standard header files.
  • Improve performance and precision of the strcmp and strncmp builtin with imprecise arguments. Fix soundness bug when strcmp is called on imprecise arguments.
  • Allow to set the bits of variable addresses with attribute “tis_address_width”.
  • Rename option -val-printf-accept-compatible-integral-types to -val-printf-accept-equisized-integral-types.
  • The once popular but non-standard Mach u_intXX_t types declared in <sys/types.h> will be declared if TIS_PROVIDE_MACH_TYPES is defined during preprocessing.
  • Take into account the implicit blocks associated with selection and iteration statements in C99 and later (see 6.8.4:3 and 6.8.5:5 in C17).
  • Improve the tis_check_leak builtin: now it detects cycles of memory that are leaked.
  • Optimize and fix the support of the trigonometric tan function
  • The deprecated tis-info-coverage tool is no longer available. Use tis-aggregate to replace it.

TrustInSoft Analyzer++

  • Improve readability of STL containers.
  • Kernel option -enum is now partially supported in the C++ plugin. The default behaviour (in the absence of that option) is to follow the C++ standard; option values “int” and “gcc-short-enums” behave as documented, and option value “gcc-enums” has no effect.
  • Preprocessing of C++ files always uses the -cxx-cpp-extra-args option. There is no fallback to -cpp-extra-args anymore when no -cxx-cpp-extra-args option is specified.

GUI

  • The ergonomic design of the “Values” widget has been slightly improved.
  • The “Values (legacy)” and “State Explorer” deprecated widgets have been removed.
  • Animations can now be disabled by adding the “graphics=low” parameter in the URL used to access the GUI. Example: http://localhost:12345?graphics=low

Release 1.40

TrustInSoft Analyzer

  • Full support for the alias attribute on functions and variables.
  • Reject invalid _Generic violating the contraints of C11 6.5.1.1.
  • Change the format of the alarm emitted when an overflow occurred in a conversion from a floating-point to an integer.
  • The efficiency of builtins for strlen, strchr, wcslen and wcschr was improved and crashes fixed.
  • New option -remove-volatile-locals to remove the qualifier “volatile” from all local variables of given set of functions.
  • Preliminary support for swprintf.
  • Support for universal characters uxxxx and Uxxxxxxxx in string and char literals.
  • New MIPS and RISC-V machdeps.
  • The x86_16 machdep has been split into x86_16, with 16-bit near pointers, and x86_16_huge, with 32-bit huge pointers.
  • Add support for C builtin types __int128_t and __uint128_t for GCC-64 bits machdeps.
  • Improve precision and performance for strcpy, strcat and printf functions.
  • All the deprecated Frama_C_xxx builtins now have an equivalent named __tis_xxx or tis_xxx.
  • Add new builtin tis_detect_imprecise_pointer, that makes the analyzer exit when any expression is evaluated to an imprecise pointer that involves a given base address.
  • Fix a bug in the detection of overlapping source and destination in strcpy.
  • The operation (char*)0 + 0 is now forbidden. The new option -allow-null-plus-zero allows it. The new predicate inside_object_or_null is added such that inside_object_or_null(p) is defined as inside_object(p) || p == \null.
  • Add a new way to represent floating-point values that handles infinities and NaNs (see section “Floating-point” of the documentation).
  • New options -enomem-value and -erange-value to specify the value of the ENOMEM and ERANGE errnos.
  • Implement detection of overlapping source and destination in s*printf functions.
  • An unverified annotation with the ‘UB’ label is now handled as an alarm.
  • GCC attribute mode(xx) is now recognized on variable declarations, in addition to typedefs, and on floating-point types as well.
  • Support options -warn-signed-downcast and -warn-unsigned-downcast in value analysis.
  • Support ‘%m’ modifier in format strings.
  • Added support for __builtin_{huge_val,inf}{,f,l}().
  • Add new option -val-exit-on-reaching-max-mem, that makes the analyzer exit as fast as possible with code 124, whenever the Value Analysis allocates more memory than the environment variable TIS_KERNEL_MAX_MEM indicates (in GiB).
  • Accesses to volatile variables are no longer considered as uninitialized accesses if they are initialized.
  • Header files for zlib (zconf.h and zlib.h) are now provided.
  • Corrected and improved type conversion when handling initializers, e.g. initializers with function calls like struct { double a; } x = { tis_interval(1, 2) };.
  • The tis_show_each builtin is now declared as a variadic function with a mandatory string as first argument. Calling tis_show_each_xxx (i.e. with a suffix) still works though, but it still has to be declared (as before).
  • The option -val-profile has been updated:
    • For some profiles, flags are now available with the following syntax: -val-profile profile:flag1,flag2.
    • The detailed help can be obtained with -val-profile help, displaying the list of available profiles and their associated flags.
    • The profile interpreter-no-mem has been removed, see instead the flag no-mem below.
    • Add a new profile analyzer with three flags. See more about these flags with -val-profile help. This profile replaces the set of options enabled by the tis-analyzer script.
    • The profile interpreter now includes the analyzer profile and now two additional flags:
      • no-mem, which is the equivalent of the former profile interpreter-no-mem
      • no-builtin, which allow to not set the list of recommended builtin for the interpreter mode.
    • The profile interpreter now enforces the -no-fs-error mode.
  • The option --interpreter of the tis-analyzer script has been updated to use the no-builtin flag of the interpreter profile (see the option -val-profile) when the option -no-tis-libc is also given on the command line.
  • Add new -dump-cmdline and -dump-cmdline-output options to print the command line used to run TrustInSoft Analyzer by expanding any meta-option that sets other options (such as -val-profile).
  • The integrated web server (used for the GUI) has been strengthened and will no longer stop when a system error occurs.
  • New tool: tis-aggregate collects results from several analyses and generates syntheses such as overall Value analysis coverage for instance. The tis-info-coverage tool and -info-reachable option are deprecated.
  • Support for lifetime of VLA of dimension 1.
  • Make the axiomatics for string.h consistent and minimize its trusted base. This means that any WP proof may need to be replayed to ensure that the proofs still hold.
  • The management of the command line options has been improved to be more predictable. The documentation has been updated according to these improvements in the section: Reference manual > Command line Options. Beware: complex command lines may have a slightly different behavior, especially if the -tis-config-load option was used among other command line options. Learn more about the new behavior of such options in the documentation section: Reference manual > Command line Options > Evaluation order > Meta-options
  • For the command line options, in the syntax for collections, the optional + character is no longer interpreted as a special character to add an element in the collection. For instance, -val-use-spec=-@all,+f should now be written -val-use-spec=-@all,f.
  • With option -val-warn-pointer-arithmetic-out-of-bounds (set by default), when pointer arithmetic such as ptr+ofs occurs, ptr must now already be a valid-or-one-past pointer.
  • Support for GCC __builtin_choose_expr.
  • Fix the behavior of the strtou{l,}l builtins (used only in interpreter mode) and implementation (analyzer mode) to match GNU libc behavior.
  • Improve the type mismatch messages of printf functions. The diagnostics of printf functions are now more explicit: “argument a has type my_integer, which is an alias for long, but format indicates int”.
  • Remove the journalization feature (it was incomplete and not really usable) and its associated options -journal-enable, -journal-disale, -journal-name.
  • Add support for GCC __builtin_{isfinite; isfinitef; isnan; isnanf} and add tis_nan and tis_nanf builtins. These are useful in TIS_ADVANCED_FLOAT mode.
  • The environment variable TIS_KERNEL_MEMORY_FOOTPRINT can be used to set the size of caches used during the value analysis, speeding up some slow analyses in which the caches were getting thrashed. The default is 2 and each incrementation doubles the size of caches. Only use this variable if you are not already low on memory.
  • Improved performance of the value analysis, especially for programs that call free or realloc.
  • Add -allow-null-lt-null to allow comparing null pointers with relational operators.
  • New option: -context-uninitialized-extern to consider the global variables that are declared and not defined as uninitialized.
  • Adopting a stricter view of pointer comparisons, comparisons with < or > involving NULL are now reported as alarms.
  • Avoid duplication of user-level UB-labeled alarms.
  • Support for GCC and MSVC extensions allowing initializers for flexible array members.
  • Improve the precision of sprintf builtin for imprecise arguments.
  • Add the -compilation-database option to be able to read compile_commands.json files, containing information about how to pre-process source files. See more about this option in the “Prepare the Sources” section of the TrustInSoft Analyzer Manual.
  • Add the -cpp-command-file and -cpp-extra-args-file options to specify a pre-processing command and arguments for the given list of files. See more about these options in the “Prepare the Sources” section of the TrustInSoft Analyzer Manual.
  • Add the -from-no-compute option to disable the dependencies computation. Notice that several computations fail when the dependencies are not available (see below).
  • To optimize computation time and memory, tis-analyzer no longer tries to automatically infer which analyses to perform. Many options now fail if -val is not on the command line such as -deps, -calldeps, and options from several plugins such as: PDG, slicing and impact analysis.
  • Improve precision of bitwise or (C and C++ binary operator “|”) between imprecise operands.
  • Full support for the static type qualifier in array size in parameters according to C11-6.7.6.3p7.
  • Add missing alarms when comparing with == pointers one-past literal strings that could be shared or not by the compiler in an unspecified way. Example: “a”+2 == “a”+2 has an unspecified result because the compiler is free to share the strings or not. Now, an alarm is emitted for this comparison.

TrustInSoft Analyzer++

  • Non-templated global namespace variables are not mangled anymore, following Itanium ABI.
  • Recursive function clones are now demangled.
  • The standard library namespace is now mangled as St and displayed as std:: instead of std::__1::.
  • Template parameter packs are enclosed between [ ] when demanling.
  • Uses of new[] causing objects larger than PTRDIFF_MAX will now trigger an alarm during the value analysis.
  • Implement function mangling as required by N4659[temp.over.link]. This fixes some symbol name clashes at link-time.
  • Arguments that are trivial for the purpose of calls are now passed by copy to match C calling convention.
  • Add a section about mangling in the user manual.
  • New option -cxx-filt <name>. It prints the unmangled version of <name> and exits.
  • Support for ACSL++ contracts attached to friend functions.
  • Large performance improvements in annotation handling.

GUI

  • The time for the GUI initialization has been reduced, especially when the tis-analyzer command is run in a directory with a lot of sub-directories (such as $HOME)
  • The “Reset widget” and “Move panel to …” contextual-menus on widget panel headers have been removed.
  • The “Allow source code edition” menu has been moved to the “Options” window.
  • The “Display” button and its deprecated “Save GUI Config As…” and “Load GUI Config…” sub-menu items have been removed.

File System

  • The widget performance has been improved: data are now computed lazily according to what the widget displays.
  • Fix a bug when checking (resp. unchecking) a file was not always added (resp. removed) in the list of files to parse.

Interactive code

  • Clicking in the interactive code when the location in the source files is a symbolic link now correctly opens the linked file.
  • Changing the font size of the Interactive code from the Options window now correctly changes the font size of opened tabs.
  • Clicking on a Inspect ... button now also focuses the Values widget.

Overview

  • Clicking on the <x> potential undefined behaviors have been found text now also focuses the Values widget instead of the Analysis review one, in order to be ready to inspect the first alarm shown (also shown when the text is clicked).

Source code

  • The syntax used to search files in the Find file button menu has been changed to be closer to the one used in Unix shells (single wildcards (*) are also allowed).

Values

  • Fix the emission ranks available in “Per callstack”, “Per Call” and “Per path” views.

Configuration Files

  • Add a new field to select the language (C or C++) to use. This language will set a list of other options to correctly analyze the program according to this language. The value auto is also accepted to automatically choose the language according to the given list of source file.
  • BREAKING CHANGE: By default, if the language field is not given, the behavior is the same as the value auto. Note: the automatic detection of the language is only performed when a configuration file is read, hence when the -tis-config-load option is given. The old default behavior can be obtained by setting the value of the language field to c.
  • The field value-profile has been updated according to the new profiles and flags: interpreter-no-mem is no longer valid and new values are available. See more in the documentation section: Reference Manual > Configuration files > Syntax > List of simple option > value-profile.
  • The field filesystem.system_errors has now the value of the option -fs-error (or -no-fs-error) as the default value (instead of true).
  • The raw_options field is now deprecated and may be removed in a future release. Any tuning option of the analyzer is now supported as a regular field. For instance, { raw_options: { "-ulevel": "150" } } can now be written { "ulevel": 150 }. See more in the documentation section: Reference Manual > Configuration files > List of options > Command line options.
  • The following fields are now deprecated and the equivalent field related to their command line option should be used instead:
    • compilation_cmd (use cpp-command or cpp-extra-args instead)
    • compilation_database (use compilation-database (with a hyphen) instead)
    • malloc-plevel (use val-malloc-plevel instead)
    • merge-after-loop and merge-after-loop-per-fn (use val-slevel-merge-after-loop instead)
    • results-by-slevel (use val-slevel-results instead)
    • slevel-per-fn(use val-slevel-function instead)
    • split-return (use val-split-return instead)
    • split-return-per-fn (use val-split-return-function instead)
    • stop-at-first-garbled (use val-stop-at-nth-garbled instead)
    • stop-at-nth-alarm (use val-stop-at-nth-alarm instead)
    • value-profile (use val-profile instead)
    • whole-graph (use whole-program-graph instead)
  • Add support for options -cpp-command-file and -cpp-extra-args-file in the “files” field. See more in the documentation section: Reference Manual > Configuration files > List of option > Option files.

tis-mkfs

  • When using the -generic option with the same value for the min and the max, the generated virtual file system does not use the tis_unsigned_char_interval function anymore, so it can now be analyzed in the interpreter mode.
  • Better error handling when opening files larger than the predefined max size.
  • Add umask implementation.

tis-make

  • tis-make and its associated documentation is deprecated and is not part of TrustInSoft Analyzer any more.
  • A replacement tool for tis-make is to use bear that can be installed with the system packet manager (typically sudo apt install bear).
  • The documentation has been updated to describe the new workflow using both bear and a tis.config file (see section User Manual > TrustInSoft Analyzer Manual > Automatic Preparation in the documentation of TrustInSoft Analyzer).

Release 1.39

TrustInSoft Analyzer

  • New option -val-profile <profile>. According to the given profile, this option sets the value of several options to make easier some analyses. The different profiles are: default, interpreter and interpreter-no-mem. See tis-analyzer -value-help for more information about profiles.
  • Scripts tis-interpreter and tis-interpreter++ are now deprecated. Use tis-analyzer --interpreter or tis-analyzer++ --interpreter instead. The --interpreter option is an alias for -val -val-profile <profile> where the profile is determined according to the other command line options. By default, the profile is interpreter-no-mem, however if an option that requires analyses results is given (such as -info-results or -gui), the profile will be switched to interpreter.
  • The tis-analyzer command no longer prints the results of the Value Analysis at the end of the computation, use -val-print to restore the previous behavior.
  • Provide a tis-modifications tool to help to track the source code modifications.
  • The tis_inject_file builtin may be used to build an array and load the content of a file in it. tis-mkfs automatically uses this builtin to inject the content of files into the analysis. The immediate consequence is that the tis-mkfs generated source file is now much smaller and loading large files is much more efficient in terms of memory and time. The previous behavior can be restored with the tis-mkfs -content-as-array option.
  • The tis_dump_each_file_xxx(…) builtin (with a suffix) is deprecated; use tis_dump_each_file (“xxx”, …) instead.

TrustInSoft Analyzer++

  • The documentation has been updated with the ACSL++ reference manual (see the “Reference Manual” section).

GUI

  • Interactive Code: a new hint button has been added to increase the value of the -val-malloc-plevel option when a weak base is involved in an alarm.
  • Analysis Settings: a new check box has been added to enable or disable the interpreter mode.
  • Analysis Settings: a new field has been added to tune the -val-malloc-plevel option. Note: once the malloc plevel value is updated, the Value Analysis has to be run again to take into account this value.
  • Virtual File System: the widget has been improved. The call to tis-mkfs is now automatically done if necessary before running the Parsing operation. The support for tis-mkfs abstract fifo, abstract character devices and generic files has been added.
  • Configuration files: the field filesystem has been changed and is not fully backward compatible. See more in the documentation section: Reference Manual > Configuration files > Syntax > List of simple options > filesystem.

Release 1.38

TrustInSoft Analyzer

  • Extend JSON format for the option -info-json-results. See the documentation for more information.
  • Improve performance of large value analyses.
  • The result of tis_dump_each_file can now be sent to either a text file (as before), or a JSON file, or both, thanks to the -val-dump-destination option. Moreover, the -val-dump-directory can be used to choose the destination directory.
  • Reject overlapping case ranges (gcc extension).
  • Change the type of the cardinal argument of the tis_watch_cardinal builtin to unsigned long long, in order to allow higher limits.
  • Fixed bug involving arrays of size 0 (GCC extension).
  • Warn if the final string character ‘0’ of source and destination overlap in strcpy, strcat builtins.
  • Fix soundness bug when a function’s argument is the value of a global variable or a struct and the function also modifies the global variable or the struct.
  • Fix a backtrace error raised when function addresses are used in loop conditions.
  • Improved handling of variadic functions taking structs as argument.
  • New option -val-clone-on-recursive-calls-max-depth. This option limits the depth at which recursive functions are analyzed when -val-clone-on-recursive-calls is set.
  • Support for Clang/GCC enumerator attributes. They are dropped with a warning, as their presence does not impact the semantics of the code.
  • Add correct support for %12c in printf functions. The effects of sprintf when applied to imprecise arguments are modeled more precisely.
  • Fixed soundness bug when a bit-field is passed as argument to a variadic function.
  • Improve printf-family functions: reject %+u and other tweaks.
  • Most functions of math.h are now mapped by the tis-analyzer and tis-interpreter scripts to builtins. Existing scripts that use the -val-builtin option may remove this option.
  • All legacy Frama_C_xxx functions related to math.h functions are renamed to tis_xxx.
  • Builtins tis_scanf and tis_sscanf are renamed tis_scanf_interpreter and tis_sscanf_interpreter. They were never intended to work in non-interpreter mode.
  • When alarms are raised in the libc implementation, an alarm is also generated at the call site in the user code.
  • Any use of a FILE* pointer after calling fclose is now detected.
  • The tis_builtin.h file can be included even when the -no-tis-libc option is used.
  • With the new -info-stmt-no-reduction option, the ‘more’ column of the ‘test’ statements information holds the ‘no reduction’ value when the states are the same in both branches.
  • If the -gui option is used, tis-analyzer now defaults to -no-val-print. In order to get value analysis results displayed on the terminal, explicit addition of -val-print is needed.
  • The –timeout option can be used to stop the Value analysis after a given amount of time.
  • The behavior of the option -time has been changed. This option now records the time performance of the analyzer while parsing files and during the Value Analysis and display the summary in the standard output at exit. The former behavior can still be obtained with the command: “/usr/bin/time -o= -a -p tis-analyzer ”. See “man time” for more information about the “time” program. Note: for some operating systems, the location of the “time” program may differ.
  • Option -time is enabled by default with tis-analyzer. Use -no-time option to disable this behavior.
  • Add options -time-verbose, -time-output and -time-flamegraph, related to the new -time option behavior.

TrustInSoft Analyzer++

  • Add support of std::exception_ptr

GUI (beta)

  • In the Overview panel, the coverage of statements is now relative to the covered functions.
  • In the Overview panel, it is now possible to save the current configuration into a file with the ‘Download’ button near the configuration fields.
  • In the interactive code, it is now possible to click on intermediate offsets of an lvalue. For instance with the lvalue “a.b.c.d”, only “a” and “a.b.c.d” were clickable. Now “a.b” and “a.b.c” are also clickable.
  • Jumping to callers in presence of recursive calls is not reflecting the path of the analysis. The list of callers and callees has been fixed in such cases.
  • In the Current Function panel, the three columns ‘Total #Called’, ‘Self time’ and ‘Total time’ have been added. These columns are by default hidden and contain the same information as the ones in the Functions panel.
  • Tabs in the Interactive Code now persist (when possible) after reparsing. For instance, if a function does no longer exist after reparsing, its tabs will be automatically closed if it was opened.
  • The “Copy mangled name” contextual menu now appears under the “Copy” one when a C++ identifier is clicked with the right mouse button. The mangled name of an identifier is used in some case, such as the evaluation of terms in the “Values” panel or for the values of command line options (such as “-slevel-function”).

Release 1.37

TrustInSoft Analyzer

  • Fix off-by-one error in strnlen builtin where a warning would be emitted for correct uses of strnlen.
  • New ppc_64, aarch64 and aarch64eb machdeps, for 64-bit POWER and AArch64 in little-endian and big-endian modes. These machdeps also have gcc_* flavors to enable gcc extensions.
  • Fix more bugs in the strnlen builtin, when size is 0 or when size is not a singleton (analyzer mode).
  • Support for ‘#pragma pack(0)’ and fixes for the semantics of #pragma pack(push,n)
  • Reject during typing the invalid C programs that try to declare functions that return arrays or functions.
  • Fix spurious warnings when functions without body return a _Bool.
  • For the tis-interpreter script, a new option –keep-results has been added to not discard the Value Analysis results which is done by default.
  • Add option -pre-file to parse a file before any other files (including pre-registered files used as runtimes)
  • Support tis_print_abstract_each function that accepts addresses as parameters, and prints the abstract value at each address.
  • Precise support for the analysis of programs that access the environment variables with the standard library (getenv, setenv, …).
  • Set the default value of option -warn-decimal-float to ‘none’ so that by default the analyzer does not warn about floating-point constants which cannot be exactly represented;
  • Machdep can now specify the underlying type of max_align_t.
  • New sparc_32, gcc_sparc_32, sparc_64 and gcc_sparc_64 machdep for 32-bit and 64-bit SPARC platforms.
  • TIS Analyzer now knows that the addresses of variables are aligned according to their types. For instance (uintptr_t)&x & 3, where x is an int variable, evaluates to 0.
  • When using the provided library (-tis-libc), in functions that call calloc, as long as the slevel settings allow it, the valid pointer and the null pointer returned by calloc are now propagated separately for better precision.
  • The former option ‘-isystem’ to overload the libc headers has been renamed ‘–custom-isystem’. The option ‘-isystem’ is now just an alias such as the ‘-I’, ‘-D’ and ‘-U’ options.
  • Improve localization and messages for syntax errors in C programs.
  • C11 atomic builtins no longer force their argument to be volatile.
  • Add the -info-results options to print to the log file a summary of a Value analysis important results that were previously only available from the GUI “Analysis review” panel. The result of the -info-precision and -info-exits options changed a little to be integrated in this summary, and the -info-exits option is deprecated in favor of -info-msg-key results:exits (more details in the documentation).
  • The information in the “Reachable” column of the -info-statements results is now more precise on the statements that include blocks (if, loops, switch, blocks). Some of these statements that were marked ‘unreachable’ before may now have a different information if some of the statements inside the block(s) are reachable (goto). Some of these statements that were marked ‘reachable’ before may now be marked ‘non-terminating’ or ‘never-terminating’. This information can also be seen in the GUI.
  • The behavior of the analyzer regarding the filesystem model has changed:
    • the ‘-fs’ option now takes a parameter which is the name of the .c file generated with ‘tis-mkfs’.
    • when the ‘-fs’ option is not set, the default behavior is now to use the model of a filesystem with /dev/stdin (readonly), /dev/stdout and /dev/stderr write only.
    • the ‘-no-fs’ option may be used to get the old default behavior (i.e. no hypotheses about the filesystem at all).

TrustInSoft Analyzer++

  • The C++ plugin has been renamed to CXX. As a consequence, the option -fclang-cpp-extra-args has to be changed to -cxx-cpp-extra-args.
  • Class invariants are now translated as pre- and post-conditions on all public instance methods of the class.
  • Copy constructors are now demangled as CtorC and move constructors as CtorM.

GUI (beta)

  • Pre-processing and Exploration Overview panels have been reworked into a single panel which is now available in all modes.
  • The “Values” widget has been reworked to include both former “Values” widget and “State explorer” widget’s features. The former “Values” widget and “State explorer” widget are still available in the “Workspace” menu. The former “Values” widget has been renamed “Value (legacy)”.
  • Two new widgets have been added to display the messages printed on the standard output and standard error by the analyzed program. These widgets are shown only when the Value Analysis is computed, and by default in the Exploration mode.

Release 1.36

TrustInSoft Analyzer

  • Support for C11 _Generic expressions.
  • Improved the modelization of malloc when slevel is used for case analysis.
  • Allow arbitrary constants for local slevel annotations.
  • Unknown functions passed to -val-builtin are no longer fatal errors, as if -permissive had been passed.
  • Replace -val-disable-constructors with -disable-constructors. Constructors are now syntactically called in the body of the entry point.
  • Fix crash when \result was used in an assigns clause.
  • Fixed bug when analyzing programs using malloc() and free() with -memexec* options.
  • Change the technical term previously shown for values into plainer
  • Support for 128 bits integers in WP.
  • Add support for C11 char16_t and char32_t literals. Correctly compute sizeof of wide strings.
  • The old -tis-config mechanisms have been replaced by the -tis-config3 ones, and -tis-config3-* options have been renamed into -tis-config-*. Learn more about these options with “tis-analyzer -server-help” in the “Analysis Configuration” section and in the Documentation in the “Reference Manual” section.

TrustInSoft Analyzer++

  • New script tis-interpreter++ to invoke the interpreter on C++ files

GUI (beta)

  • UI: The mode (Pre-processing, Exploration, …) can now be changed during the Value Analysis.
  • UI: The GUI can now be used while the analyzer is parsing the files, and the parsing progress is now displayed.
  • Interactive code: more information, when available, about alarms is now available by clicking on the ‘+’ button aside the ‘assert’ keyword. Alarms impacted by this change are: function_pointer, unclassified.
  • Pre-processing and Exploration Overview panels have been reworked into a single panel which is now available in all modes.
  • Analysis Review panel is now also available in the Value Analysis mode.
  • Value Analysis: Command line options “-val-stop-at-nth-alarm” and “-val-stop-at-nth-garbled” can now be set from the GUI from the “Value Analysis” mode.
  • The “Values” widget has been reworked to include both former “Values” widget and “State explorer” widget’s features. The former “Values” widget and “State explorer” widget are still available in the “Workspace” menu. The former “Values” widget has been renamed “Value (legacy)”.

tis-mkfs

  • Options -nb-max-files/dirs have been removed.
  • New options -nb-max-created-files/dirs: they allow the analyzed program to create new files/directories up to the given limit. These limits do not include the number of files in the generated file system from the use of other options.
  • The stdio functions are now implemented even when tis-mkfs is not used.
  • The content of the stdin stream is mapped to the tis-mkfs-stdin special filename.

Release 1.35

TrustInSoft Analyzer

  • Improve simplification of compile-time constant expressions involving some floating-point constants (useful, for example, for computing the size in array declarations).
  • Improve *printf builtins to recognize the known length taken by an unknown printed argument although the argument itself is not known precisely.
  • Allow use of -val-args without -val-interpreter-mode
  • Imbricated axiomatics are now supported.
  • Fix analyzer crash when left shift << is applied to a value of enum type.
  • Fix issue when lvalues, the contents of which have been set through heterogenous pointer casts, are passed as argument to v*printf functions.
  • Replace option name -val-abort-on-pointer-library-function with -val-stop-on-pointer-library-function.
  • Provide an implementation for __builtin_clzll.
  • New option -integer-constants to tell the front-end how to choose the types of integer constants. The default is to follow the C99 standard strictly.
  • Improve *printf builtins to detect misuse of %h{d,u,x} and %hh{d,u,x} formatters.
  • Fix unsoundness with sprintf for imprecise arguments.
  • Fix crash when an address seems to be passed as ‘size_t’ for functions: memchr, memcmp, snprintf, strchr, wcschr, strncmp, wcsncmp, strnlen, wcsnlen.
  • Clarify the message logged when a function pointer being applied seems not to point only to valid functions
  • Set option -val-malloc-returns-null by default.
  • Rename option -tis-info into -info.
  • New “never-terminating” possible value in the “Reachable” column of the -info-statements results (can also be seen in the GUI).

TrustInSoft Analyzer++

  • Loop pragmas are now supported in annotations.
  • Detect and add STL runtime files automatically. This behavior can be disabled with the -cxx-noruntime option.
  • Statement contracts are now allowed and parsed.
  • Parse C++ runtime files after all other files.
  • Add option -no-val-malloc-returns-null by default.

GUI (beta)

  • Analysis Review mode has been merged into the Exploration mode.
  • Templates of the “Workspace” menu have been removed. In the Exploration mode, the default shown widgets are the one of the removed Semantic template.
  • New feature: Some hints and shortcut buttons have been added directly in the interactive code. For instance, these buttons may help the inspection of some alarms. More shortcuts will be added in the future. These buttons can be hidden/shown by right-clicking on the interactive code background.
  • The “Evaluate ACSL Terms” widget has been renamed “Values” and is now available from the Analysis Review mode.
  • The “Getting Started” widget in the Pre-processing mode has been re-designed and renamed “Overview”.
  • The “Parsing & Linking” widget in the Pre-processing mode has been moved to the left panel and is now shown when an error occurred during the parsing operation or when a file is selected in the File System panel.
  • Interactive Code: long C++ identifiers are now displayed in an elided version and can be expanded by clicking on the ellipsis at the left of the identifier.
  • In callstacks: long C++ identifiers are now displayed by default in an elided version. The full identifier can be shown with the associate option in the “Options” window.

tis-mkfs

  • Set the pre-allocate mode to use a statically allocated array for storing data, ie the macro __TIS_MKFS_STATIC_ALLOCATE is set by default.
  • Show message in the log file when the application calls write, fwrite, pwrite, puts, fputs to stdout (similar to printf).

Release 1.34

TrustInSoft Analyzer

  • New option -val-allow-left-shift-into-sign-bit: do not emit an alarm when a 1 is shifted into the sign bit (C++14 rule)
  • When relying on a function’s contract to infer the effects of a function, an ‘assigns’ clause assigning to an lvalue of type _Bool only causes the value analysis to assume that the lvalue receives an unknown value in {0, 1}.
  • Add basic support for the modulo operation in ACSL of the form ‘term_lval % integer_constant {==, !=} integer_constant’ (and the other way around).
  • [Value] Fix the semantics of volatile qualifier during calls to memset and memcpy.
  • When the value of an unknown variable of type ’_Bool’ has to be inferred (‘extern’ variable, argument of the entry point, or ‘-lib-entry’ option), use {0, 1}.
  • Fix complexity issue during parsing of imbricated ternary operator ? within loop and function calls.
  • New {gcc_,}arm{,eb}_eabi machdep for ARM targets in little- or big-endian mode, using a generic compiler or gcc.
  • Improve printf builtin for %s in analyzer mode so that an alarm is emitted only on non-nul-terminated strings.
  • Generated assigns clauses are now pretty-printed with an explicit ‘generated’ label. The location of the warning emitted when an assigns clause is generated is now the location of the declaration of the concerned underspecified function. It used to be the location of the function call.
  • Improve performance of source-level link.
  • Introduce the ‘tix_cxx_weak’ attribute that allows functions with this attribute to not comply with the “there shall be no more than one external definition for each identifier” rule (C11:6.9p3). A (non-static) function with the same name can be redefined many times in multiple files, provided that all these (re)definitions contain exactly the same body and have the ‘tis_cxx_weak’ attribute attached.
  • Some expressions without side-effects “e;” could be erased by the front-end, and when this happened, undefined behavior hidden in these expressions would fail to be detected by the analyses. Now, all expressions are preserved, so that the undefined behaviors that they may contain are detected.
  • Reject programs that use floating-point computations as array sizes, e.g. int samples[1 + (int)(TIME / FREQUENCY)]; where TIME and FREQUENCY are macros for floating-point values.
  • Fix semantics of ‘-volatile-globals’ option to match its documentation.
  • Fix handling of the ‘alias’ attribute: a prototype for the alias target function is generated (if needed) just before the function which has the ‘alias’ attribute attached.
  • Fixed soundness bug when applying ‘printf(“%s”’ to an unknown buffer that might not be zero-terminated. An alarm is now emitted.
  • add tis_memset_bounded() and tis_memcpy_bounded(), variants of memset() and memcpy() with extra upper bound arguments, which may be used with Value get to more precise results.
  • The analyzer now stops the ongoing analysis if it encounters a function with no body and no specification that manipulates pointers. It was never a gain of time to try to continue when this situation happens. The old behavior can be obtained with the option ‘-val-continue-on-pointer-library-function’.
  • Add -I${FC_SHARE}/mt as default for -cpp-extra-args. This spares the user from having to manually provide the path to pthread-related system headers.

TrustInSoft Analyzer++

  • Support for all first-order ACSL++ logic builtins.
  • Improve performance on large source code.

Release 1.33

TrustInSoft Analyzer

  • Detect indeterminate arguments to builtin functions even if a body is also present for these functions.
  • New -language option which lets the C++ plug-in ignore files it would normally process due to their extension.
  • The -val-warn-pointer-arithmetic-out-of-bounds option is now set by default.
  • Add option ‘-U ’ to ‘tis-analyzer’ as a shortcut for -cpp-extra-args=“-U”.

TrustInSoft Analyzer++

  • Properly destruct the variable declared in a for loop condition at each iteration.
  • Make local declarations in catch, for, if, switch and while, as well as captured variables in lambda, accessible to annotations.
  • Object fields declared as mutable will cause const objects to be cast into their non-const equivalents when used as lvalues.
  • Properly destruct temporaries in a while condition at the end of each iteraton.

Release 1.32

TrustInSoft Analyzer

  • Add -no-tis-libc option to tis-interpreter. It can be used to analyze libc functions or to provide custom libc implementation.
  • The tis-analyzer -no-tis-libc option now doesn’t load the tool libc builtins anymore.
  • Syntactic support for _Atomic C11 keyword

TrustInSoft Analyzer++

  • Beta release of TrustInSoft Analyzer++

GUI (beta)

  • Add a widget to allow the user to change the machine architecture in the Pre-processing Mode

Release 1.31

TrustInSoft Analyzer

  • Add attribute tis_cleanup(f(I)) for array declarations where f is a function cleanup similar to GCC cleanup function and I is an integer literal denoting the number of cells of the array cleanup. The integer is optional and when it is missing acts tis_cleanup acts like GCC cleanup but is not impacted by the machdep.
  • Aligned the inline functions handling with the C11 standard and the compilers behavior. Added the “inlining-mode” option which allows to specify how inline definitions should be handled.
  • Add __int128 type support on a per-machdep basis, currently limited to gcc_x86_64.
  • Add option -keep-unused-static-functions (opposite -remove-unused-static-functions).
  • In order to allow parallel installations of Frama-C and TIS-Analyzer without any risk of interference:
    • all ‘frama-c’ binaries have been renamed ‘tis-kernel’
    • all “FRAMAC_” environment variables have been renamed “TIS_KERNEL_
  • New option “-tis-libc” (and “-no-tis-libc”): it adds (resp. remove) the TrustInSoft Analyzer libc runtime. This option is also available with “tis-kernel” and is set by default with “tis-analyzer”. The “tis-analyzer” option “–no-libc” has been removed.
  • The C functions ‘sin’ and ‘cos’ are not anymore bound to built-ins by default since the user may choose between two different versions according to his needs.

TrustInSoft Analyzer++

GUI (beta)

New Features

  • New option -tis-config and -tis-config-dir: When set, the configuration for the analysis done in the GUI is automatically saved in the given directory (default “./.tis”). When the analyzer is run and a configuration directory already exists, the configuration is automatically loaded. However, it is not recommended to edit files in this directory while TrustInSoft Analyzer is running.
  • Source Code:
    • Add a button “Find file” in order to search and open an existing file accessible from the analyzer. This search feature comes along with auto-completion.
  • New widget: Grep
    • This widget offers a new syntactic whole source code pattern search feature.

Improvement

  • Source Code:
    • Source files are now loaded lazily in the GUI. This will greatly improve performances when a lot of tab are opened in the Source code panel.
    • Source file tabs are now kept after parsing files and even among two different sessions of TrustInSoft Analyzer if the files have the same name.
  • Import/Export Sources:
    • When uploading a file with a name that already exists in the File System, the uploaded file will no longer be renamed. Instead, a confirmation window will ask the user if the uploaded file should be ignored or should overwrite the existing one.
  • New Mode: Value Analysis. The old “Value Analysis” window has been refined into a mode and allows to browse the interactive and source code more efficiently.
    • Changing the Value Analysis options will no longer reset the Value Analysis current results
    • The syntax of the configuration files used by the option “-tis-config” or with the tab “Import/Export Settings” of the Value Analysis mode has been changed. These files are still human-readable and editable but backward compatibility with the previous TrustInSoft Analyzer versions (< 1.31) is not supported.
  • New Mode: Analysis Review. The old “Analysis Review” window has been refined into a mode and allows to browse the interactive and source code more efficiently.
  • Show Defs:
    • A new contextual menu called ‘Show Defs [..]’ is now available. It is similar to ‘Show Defs’ but gives the list of the definitions of the locations pointed by the selected left-value.
  • Data grids: All data grids (Functions, Variables, Types, …) now filter out the libc by default

Bug Fixes

  • UI: Some identifiers are no longer truncated in the GUI
  • State Explorer: the State Explorer tab should no longer be unavailable after parsing files or running Value Analysis from the GUI
  • Parsing: fix a bug when sometimes the GUI tried to parse deleted files
  • Import/Export Sources: the GUI no longer freezes after canceling a file selection while uploading sources
  • Grids: fix minor formatting bug while downloading some data in CSV format
  • Function with a constructor attribute and builtins are now properly counted as reachable when this is the case.
  • Do not filter ‘ensures’ properties in the Analysis Review step

Documentation

  • New architecture of the documentation with the following categories: tutorials, user manual, reference manual, coding standards. If you had links that were pointing to the documentation, you may need to update them according to the new architecture.

Release 1.30

GUI (beta)

New Features

  • Introducing Modes: a mode is a workspace with dedicated widgets for a specific workflow defined by the mode, without changing the layout of the GUI. The previous version of the GUI is now available under the mode Exploration.
  • (Experimental) New Mode: Pre-processing. The pre-processing workflow is now integrated in the GUI with the following widgets:
    • The File System widget allows:
      • to browse the file system from the location where TIS-Analyzer has been launched
      • select the files to parse
      • (re)run the parsing operation
    • The Getting Started widget displays in detail the workflow to follow to achieve successfully the Pre-processing phase.
    • The Parsing & Linking widget gathers parsing and linking details (output, errors, …).
    • The Parsing Settings widget allows to change the basic settings for the Pre-processing, such as the “-I”, “-D” and “-U” options given to the pre-processor.
    • The Import/Export sources widget allows to upload/download sources from the web browser to the location where TIS-Analyzer has been launched.

Improvements

  • Analysis Review: the analysis review is now automatically computed when its associated window is shown

Bug Fixes

  • Value analysis window: the notification that warns that the Value analysis is already computed when the button ‘Run Value Analysis’ is clicked should no longer appear when the Value analysis has not been computed.
  • Evaluate ACSL Terms: fix uncaught error in the evaluation of terms in undefined function ACSL specifications

TrustInSoft Analyzer

  • Add a new script ‘tis-interpreter’ to analyze C programs in interpreter mode
  • Add a new script ‘tis-analyzer++’ to analyze C++ programs
  • Add option ‘-cxxincludepath’ to ‘tis-analyzer’ to auto-tune the path to the C++ system library.
  • In the -tis-info-function result, the ‘val-use’ column is now ‘built-in’ (instead of ‘specification’) for the built-in functions.
  • Add option ‘-fs’ and ‘-fs-no-err’ to ‘tis-analyzer’ to use tis-mkfs library.
  • Add a ‘TRUSTINSOFT_ANALYZER’ macro to the preprocessing options to help the users filter the modifications related to ‘tis-analyzer’.
  • The options can now be given in any order (no need to put ‘tis-analyzer’ options first anymore).
  • Add option ‘-I ’ to ‘tis-analyzer’ as a shortcut for -cpp-extra-args=“-I”.
  • Add option ‘-D ’ to ‘tis-analyzer’ as a shortcut for -cpp-extra-args=“-D”.
  • Add the ‘-cpp-tool’ option to choose the preprocessing tool.
  • Add the ‘-isystem ’ option to add a custom include path before the tool ones.
  • Add a ‘–custom-libc ’ option to add a custom file before the tool runtime files.
  • The ‘-ogui’ is not supported anymore.
  • The ‘-test’ option is deprecated. Use tis-interpreter instead.
  • Evaluate assigns and ensures annotations on assembly code.

Release 1.29

TrustInSoft Analyzer

Improvements

  • Documentation: minor changes.

Release 1.28

The release 1.28 is an internal release. It does not contain changes.


Release 1.27

GUI (beta)

New Features

  • Value Analysis: The dedicated window for the Value Analysis has been redesigned. This window is accessible with the button “Value Analysis” (was “Run Value Analysis) in the toolbar at the top of the GUI. It’s now possible:
    • to visualize some statistics on the analysis with charts
    • to change the slevel and the Entry point parameter
    • to change the Value Analysis advanced settings (slevel per function, merge after loop, split return strategy)
    • to re-run the Value Analysis as many times as you want
    • to continue observing the old existing statistics in the tab “Advanced Statistics”
    • to download/upload the Value Analysis settings (limited to the settings supported in this window). This feature is also available on the command line with the option “-tis-config”.
  • (Experimental) Analysis Review: A new window is now available to help the review of the Analysis done by the Value plug-in. Once the Value Analysis computed, a list of items is displayed (for example: the list of alarms, the list of unused files, the list of undefined functions reached by the analysis, …). Each item details what the user should review. It’s also possible to:
    • skip the review of some points
    • add comments on details shown at each point
    • mark a detail/point as manually reviewed
    • download the report of the Analysis Review in a text and PDF file
    • export the review configuration (all comments, review statuses, …) into a file and import it with the option “-tis-review”
    • automatically save the review configuration when TIS-Analyzer exits with the option “-tis-review-auto-save”
    • preserve the review configuration among several Value Analysis and even after reparsing source files
  • Current function: The current function’s slevel, merge after loop strategy and split return strategy can now be modified directly in this panel
  • Open global: the search function has been improved
  • Source code: Reparsing all input files is now possible with the button “Reparse File”

Improvements

  • Source Code:
    • The button to enable/disable edition in the source code has been moved to the “Display” menu in the main toolbar. Moreover, edition in the source code is now enabled by default.
    • Save/Revert buttons have been moved to the panel’s toolbar. Buttons to save/revert all files have also been added.
    • Add keyboard shortcuts for “Save File” (Ctrl+S), “Save All” (Ctrl+Maj+S) and “Reparse Files” (Ctrl+R)
  • Documentation: Add an entry about the builtin ‘tis_interval_split’ to easily propagate values separately.

Bug Fixes

  • Properties: Fix a bug where the properties locations weren’t updated after launching the Value Analysis from the GUI
  • Variables: Fix a bug where the variables list weren’t updated after launching the Value Analysis, for the first time, from the GUI
  • State Explorer: Fix a bug where the evaluation fails if the current program point is a function’s Pre or Post state

Tis Analyzer

  • Improve tis-make usability
  • If __TIS_MKFS_STATIC_ALLOCATE is defined when using tis-mkfs, the file data are statically allocated so these allocations are not reported as leaks.
  • Only the degeneration point’s statement is now marked as Degenerated. All statements above in the callstack are now marked as Unpropagated.
  • The following functions Frama_C_xxx are deprecated and are replaced by tis_xxx. For these functions, it is no more necessary to include the header <__fc_builtin.h>. In order to use the tis_xxx builtins, simply include the header <tis_builtin.h>. Below are the deprecated functions with their new equivalent:
    • Frama_C_show_xxx => tis_show_xxx
    • Frama_C_float_interval => tis_float_interval
    • Frama_C_double_interval => tis_double_interval
    • Frama_C_make_unknown => tis_make_unknown
    • Frama_C_nondet => tis_nondet
    • Frama_C_nondet_ptr => tis_nondet_ptr
    • Frama_C_interval => tis_interval
    • Frama_C_interval_split => tis_interval_split
    • Frama_C_unsigned_char_interval => tis_unsigned_char_interval
    • Frama_C_char_interval => tis_char_interval
    • Frama_C_unsigned_short_interval => tis_unsigned_short_interval
    • Frama_C_short_interval => tis_short_interval
    • Frama_C_unsigned_int_interval => tis_unsigned_int_interval
    • Frama_C_int_interval => tis_int_interval
    • Frama_C_unsigned_long_interval => tis_unsigned_long_interval
    • Frama_C_long_interval => tis_long_interval
    • Frama_C_unsigned_long_long_interval => tis_unsigned_long_long_interval
    • Frama_C_long_long_interval => tis_long_long_interval
    • Frama_C_memcpy => tis_memcpy
    • Frama_C_memset => tis_memset
    • Frama_C_abort => tis_abort
    • Frama_C_alloc_size => tis_alloc_size
  • Prevent crash of -remove-redundant-alarm when logic labels LoopEntry, LoopCurrent and Init are present.
  • [Value] Structure padding now takes unspecified value when structure is passed as a function argument or returned in a function call.- Support for GCC attribute cleanup
  • [Value] The \dangling predicate is no longer interpreted: its meaning is confusing when applied to a tset- New feature: made padding uninitialized for struct-to-struct assignments.
  • Fixed bug concerning repeated definitions of the same typedef name: in C11 redefining the same typedef name is allowed if repeated definitions denote the same type.
  • Fixed bug allowing to specify a named zero-width bit-field.
  • Fixed bug concerning invalid sizeof operands: function type, incomplete type, bit-field. Also corrected problems concerning invalid composite types.
  • Support for GCC __builtin_trap and __builtin_unreachable.
  • [Value] Fix the origin of garble-mix for leaf function.

Tis Analyzer++

  • Support for attributes in declarations.
  • Add support for variadic templates.
  • Add support for the capture by value of records in lambda expressions.
  • Add support for generic lambda expressions (C++14).
  • Add support for the init capture in lambda expression (C++14).
  • Add support for the capture by value of C-like arrays in lambda expressions.
  • Add support for C++11 lambda expressions.

Release 1.26

GUI (beta)

New Features

  • Current function: This widget now contains, in addition to the list of callers/callees, various information about the current function.
  • Current statement: This widget now contains, in addition to the list of previous/next statements, various information about the current statement.

Improvements

  • Documentation: The GUI documentation has been revised to introduce concepts used in the GUI
  • UI:
    • Panels dynamically inserted in the left area (such as the list of “Show defs” statements) are now more visible when shown
    • The toolbars at the top of the GUI have been redesigned and reworked into a single one
    • The “List of widgets” has been renamed into “Workspace” and all widgets have been classified into categories
    • The Templates values in the Workspace menu has been changed and the default template is now the Syntactic one
    • The list of Projects has been moved to a new widget “Projects” (hidden by default)
    • Two tooltips have been added to help the user discover non visible features. Each of these tooltips can be definitively desactivated with a checkbox in the tooltip. Here is the list of the tooltips:
      • At the start of the GUI to discover the Workspace menu
      • After computing Value when the selected Template is not the Semantic one to discover the Value Analysis related widgets
    • The “Edition mode” button has been moved next to the “Source code” panel’s title
    • Add a shortcut (Ctrl+O) for the “Open global” button
  • Callstacks: The focused callstack has been moved to the Callstacks panel

Tis Analyzer

  • Add builtins for the following functions: fprintf, strcat, wcscat, wcscmp, wcscpy, wcslen, wcsncmp, wcsnlen, wmemcpy, wmemmove, wprintf.
  • The -tis-info-reachable option now prints NO_RESULT when there is no information about the reachability of a function (for instance when using -obviously-terminates)
  • The -tis-info-reachable option now includes tis shared directory in libc detection (useful when using tis-mkfs) and doesn’t include libc statements in coverage.
  • The coverage information provided by -tis-info-function is now NA when the information to compute it is not available.
  • tis-info-coverage now prints the total coverage
  • add a -nb-tests option to tis-info-coverage to print the number of tests in which the function is reached.
  • The -tis-info options now print the unmangled name for functions and types in C++ programs
  • Fixed problem allowing to specify an incorrect bit-field width: a negative width or a width that exceeds the width of the corresponding type.
  • Fixed bug concerning the type of the result of pointer subtraction, it is now correctly ptrdiff_t. Also made the size of this type consistent between the C header files and OCaml machdep definitions.
  • Fixed bug concerning named structure definitions in casts which were causing “redefinition of ‘s’ in the same scope” errors due to treating the same definition multiple times.
  • Fixed bug when a signed bit-field was passed as argument to a builtin.
  • Removed option -val-show-time: more fine-grained measures are available
  • Heavily refactored the Cabs2cil module in order to make the dependencies between different parts of it more manageable.

Tis Analyzer++

  • Improve support of template generation in namespaces.
  • Explicit global namespace (leading ::) are now allowed in annotations.
  • Do not crash on “using namespace” statements in functions.
  • Virtual destructors are supported in delete and delete[] statements.
  • `extern’ const globals are no longer translated to static.
  • Local structure in templated method of templated records are corrected.
  • Symbols with extern “C” linkage will now correctly be safe from name mangling.
  • Non-public class members in ACSL annotation no longer produce spurious error messages.
  • Add support of static member in the subclass of a templated class.
  • Added support for local records in functions.
  • Mangling of local enumeration is now correct.
  • Subclass dependencies are now transmitted to their parents.
  • Loop annotations of C++ range-based for loops are now processed correctly.
  • The nullptr keyword is now recognized in ACSL++.
  • enum default values are no longer unsigned.
  • Added support for record typed init lists.
  • Arrays of members are now correctly initialized in constructors.

Release 1.25

GUI (beta)

Bug Fixes

  • UI:
    • A new button has been added above the interactive code in order to jump to a written global. The Globals panel has been moved to the bottom-right area.
    • A window can now be closed automatically when a click is done outside of the window. This change impacts the following existing windows: List of widgets, Options.
  • Interactive code: Fix a bug where bullets that indicates the properties statuses weren’t shown if Value wasn’t computed

Improvements

  • Documentation: New output theme (responsive design, grids …) for better design and readability.

Bug Fixes

  • Interactive Code: Fix a bug with ghost tabs after a Reload action for globals with the same name in C++

Tis Analyzer

  • Fix inconsistant AST due to forward declaration of arrays without a size.
  • Remove unused constructor.
  • Fixes crash with -val-clone-on-recursive-calls. Fixes functions marked in the GUI as unreachable although called with -val-clone-on-recursive-calls.
  • New option -val-warn-harmless-function-pointers, on by default, to warn for harmless mismatches between pointed function and function pointer type. Use -no-val-warn-harmless-function-pointers to let the analysis continue past, for instance, the application of a function taking a char* as argument through a pointer to function taking a void*.
  • Add tis_strto{l,ll,ul,ull}, tis_strto{d,f,ld}, tis_ato{i,l,ll} and tis_atof builtins (only intended for use with exact inputs, not for normal analyzer mode).
  • Removed legacy builtins that are now available in improved and fixed versions as tis_name instead: Frama_C_printf, Frama_C_wprintf, Frama_C_sprintf, Frama_C_snprintf
  • New option -val-warn-va-arg-type-mismatch, to toggle warning for mismatches between the type parameter passed to the va_arg macro and the actual type of the next variadic argument. It is enabled by default. Use -no-val-warn-va-arg-type-mismatch to let the analysis continue past such situations.
  • Corrected the problem appearing when a VLA (Variable Length Array) declaration contained a function call in the size expression.
  • Fixed the problem with not simplifying complex expressions in array sizes of VLA declarations.
  • Corrected the problem with emitting spurious warnings for out of bound array access when in fact the upper bound is certainly respected.
  • Fix WP output to Coq with ACSL sum type definition.

Tis Analyzer++

  • Implicitly generated default constructor can call default constructors with optional function parameters.
  • Add support of delegating constructors.
  • Improve template names and types display.
  • Improve template generation for templates referring to global variables.
  • Improve error messages for annotation syntax errors.
  • Improve handling of initializers of global and constant variables.
  • Preserve the const specifier in the generated code when possible.
  • Preserve the static specifier for pointer types.
  • Temporaries used in initialization of global references are now specified static.
  • Improve display of qualifiers in templated types.
  • Improve template generation in presence of typedef/using.
  • Support return f() when f return type is void.

Release 1.24

GUI (beta)

New Features

  • New option “-server-port-auto”: a random free unprivileged port number (between 5000 and 20000) will be chosen. When this option is set, the option “-server-port” is ignored.
  • UI: The list of widgets now allows the user to choose a template. A template is a pre-selected set of shown and hidden widgets and will show only useful widgets for the described task (Syntactic Review, Semantic Analysis, …)

Improvements

  • Interactive Code:
    • Each clickable element can now be copied to the clipboard with the right-clic menu item “Copy”
    • The display trigger of the yellow vertical left-line on statement can now be customizable in the “Options” window
    • The font size is now customizable in the “Options” window
  • Source Code:
    • The font size is now customizable in the “Options” window
  • Evaluate ACSL Terms:
    • Clicking on a function in the “Before” and “After” columns will now go to the function definition instead of changing the current term
    • The current program point is now displayed
    • A button has been added to return to the current program point, instead of clicking on a term.
    • A default program point is now chosen when the current user selection has no associated program point. When this default program point is chosen, the text that display the program point is highlighted to warn the user. This also allows to evaluate more than compile-time constants when there is no valid program point after a user selection in the interactive code.
  • UI:
    • Add a graphical feedback for grids without results instead of leaving an empty grid alone
    • Improve design of the “List of widgets” window
    • Improve design of the “Options” window
  • Documentation:
    • Add more CWE and a description.

Bug Fixes

  • Interactive Code:
    • The “Show impacting conditional” action now notifies the user when no result was found
    • Fix bug where bullets (for property statuses) weren’t always aligned with their associated property
  • Evaluate ACSL Terms:
    • Selecting a function name will no longer show an empty line/grid.
    • Fix bugs on term evaluation in ACSL comments

Tis Analyzer

  • When using the specification of a function returning a function pointer, a generated alloced_return base is no longer created and returned.
  • New version of the tis_scanf builtin. The only known limitations are: the ‘%p’ directive is not implemented; NAN, INF and INFINITY are not parsed as numerical values; and exotic format locale formatting is not allowed.
  • Add support for mixed addresses and values in tis_strnlen second argument. Add ptr validity check in tis_memchr.

Release 1.23

Tis Analyzer

  • Make -no-deps-show-progress be the default.
  • Correction of a false positive with -unspecified-access on compound litterals.
  • New option -address-alignment allows to assume an alignment of n for all base addresses. The consequence is that bitwise operations &, | and ^ between pointer representations and numbers strictly inferior to n produce precise results.
  • Added the builtins tis_ptr_is_within(void *p, void *start, void *end), which returns 1 if and only if the three pointers point to the same object and p is within the range [start ; end[ (otherwise it returns 0), and tis_ptr_is_less_than, which provides a total order for pointers.
  • New option -val-abort-on-pointer-library-function to stop the analysis as soon as a pointer-returning library function is encountered. This should help new users, as it is virtually impossible to do the right thing for a pointer-returning function without an implementation.
  • Registering twice the same machdep is now accepted
  • Add proper support for empty aggregate initializers in GCC mode
  • Meaningless assigns clauses are now rejected more agressively.
  • Operator ! applied to constant expression is no longer simplified when not required
  • Informative messages about inactive behaviors are now emitted only at verbosity level 2
  • Messages on ACSL predicates with Unknown/Invalid status are now emitted with a ‘warning’ severity, consistently with the emission of alarms. ‘True’ statuses are hidden if option -val-show-progress is unset.
  • Option -from-verify-assigns takes into account direct and indirect dependencies.
  • Distinguish direct and indirect dependencies in ‘from’ clauses to compute the effecst of an ‘assigns/from’ clause. See section 7.2 of the manual
  • Fix specifications of memchr and strncpy.
  • Fixes example of logic label use.
  • Widening hints now includes signed and unsigned limits for the bitsize of the value being widened, but does not include arbitrary limits anymore. The convergence is generally faster but results may be more or less precises depending on the case.
  • Automatic generation of assigns from GCC’s extended asm.
  • Evaluation of ACSL ranges takes into account option -safe-arrays. In particular t[..] remains within the bounds of t.
  • Take into account ‘volatile’ qualifiers on struct typedefs, which were previously ignored.
  • Support for \valid_function predicate during evaluation
  • New predicate \valid_function, requiring the compatibility between the type of the pointer and the function being pointed
  • Fix unsoundness for overflows on binary operations when one or two operands were constant (RTE plugin)
  • Fix unsoundness on unary minus expressions when option -rte-trivial-annotations is active
  • New options -then-last and -then-replace.
  • New option -remove-projects.
  • New option -set-project-as-default.
  • Removed obsolete file machine.h (along with other similar files) from the Frama-C share folder.
  • Black-list gcc’s builtin macros for logic pre-processing to avoid warnings for duplication.
  • Added ACSL specifications to some standard library functions, including read, write and realloc.
  • Correct handling of string and char constant in logic pre-processing.
  • Better overloading resolution for logic.
  • Disallow all incomplete types for struct fields

Tis Analyzer++

  • Delete is fixed on nullptr.
  • Fix a bug about subclasses of templated classes.
  • Fix bug about virtual tables and inheritance.
  • Contracts on templated function definitions are now supported, as well as ACSL annotation refering to templates arguments.
  • Added support of empty initializer list for scalar types.
  • Fix inadequate comment in templated functions.
  • Fix failure with out-of-line static const members declaration
  • Fix segfault with destructor of classes with trivial bases
  • Fix segfault with class instance used for their types only
  • For range statements are now supported.
  • Initializers of temporaries are now called at the right time.
  • Zeroing constructors are now supported.

GUI (beta)

New Features

  • It’s now possible to edit the source files directly in the GUI. The edition mode can be turned on with a button above the Source code panel. Note: you still must restart the analyzer by hands in order to take into account these changes.

Improvements

  • Source code: A warning message is emitted whenever a file shown in the “Source code” panel is not identical to the one used by the analysis
  • Evaluate ACSL Terms:
    • The function name of local and formal left-values now appears in the term information text
    • Evaluate compile-time constant without selecting any location in the interactive code is now allowed

Bug fixes

  • Fix a bug when an (false) error appears in the GUI with the message “transaction aborted”
  • Properties: clicking on a global property (axiom, axiomatic, lemme, …) now shows the property in the interactive code

Release 1.22

Tis Analyzer++

  • Better error reporting for bad comments at global level.
  • Templated class in templated class is now supported.
  • Defaulted constructors are allowed in templated classes.
  • Classes are now allowed as first member in templated classes.
  • Add the support of initializers for local variables, members, static members and global variables.

GUI (beta)

Improvements

  • Add the option “-server-expose” to be able to access to the GUI from the network without any reverse-proxy

Release 1.21

GUI (beta)

Improvements

  • Documentation: the GUI documentation has been greatly improved.
  • Plugin Value: Launching Value from the GUI without a valid entry point, or with an invalid number of arguments, now displays an information message instead of a server error.
  • Value Analysis status (Button “Run value analysis”): Functions and their callstacks are now more readable
  • Interactive code:
    • The “Create a link to this location” now displays a new window with the full link to copy/paste in order to go to this location in any browser with an access to this TIS Analyzer session.
    • Contracts of functions mapped to a built-in are now shown in the function definition.
  • Function Context: Callsites are now displayed near the caller/callee’s name when the filter “Hide callsites” isn’t active.

Bug fixes

  • Fix a GUI crash when the slevel parameter is really high.
  • Value Analysis status: Fix minor bugs

Tis Analyzer

  • Default behavior is now to be GCC compliant (as it is the case with the -32 option).
  • Changes in the handling of incomplete structs and zero-length arrays. Initialization of incomplete (completely undefined) structs is now duly rejected. Several compiler extensions to the C99 standard (empty initializers, zero-length arrays, etc.) now require a GCC or MSVC machdep (e.g. -machdep gcc_x86_32).
  • Better handling of C99 flexible array members (FAMs). Static initialization of FAMs (a GCC extension) is no longer supported.
  • New alias for Frama_C_alloc_tms: tis_alloc. Builtin tis_alloc has been implemented using true weak bases. The former builtin is still available as tis_alloc_weak_legacy.
  • The indirect dependencies must now have a label ‘indirect:’ in the \from part of the assigns properties. Warning: this may break existing specifications.
  • Support for richer arguments to align attributes.
  • Support for GCC constructors attributes during Value analysis. They will be called before the entry point is analyzed. Add option -val-disable-constructors to prevent their interpetation.
  • Fix lib-entry over-approximation for const arrays within structs.

Tis Analyzer++

  • Add the support of the using keyword in functions, classes, template specialization and template instantiation.
  • Destructors calls are correctly generated for base classes and class members.

Release 1.20

GUI (beta)

Improvements

  • Evaluate ACSL Terms: the grid has been reworked
    • The perfomance of the grid has been greatly improved: the grid is now a remote grid and will not load the callstack details if there are not shown at the screen
    • Filters are now per column and accept regular expression like all the other grids for more expressiveness
    • Download a CSV file for this grid is now possible
    • Really big values are now truncated in the grid. A link is available at the end of the truncated value in order to see its whole value. Note: filters keep to search in the whole value.
  • The Statistics button in the main toolbar has been removed: information related to this button can now be found in “time” columns in “Functions” and “Statements” panels.

Tis Analyzer

  • Better propagation strategy for nested loops. Results are usually much more predictable (and often more precise) when the loops are not fully unrolled by slevel.
  • The preconditions of functions overriden by builtins no longer receive an ’Unreachable status for calls within dead code: the specification is ignored everywhere.
  • Incorrect return statements (return void on non-void functions and vice-versa) now generate errors instead of warnings.
  • New option -val-warn-undefined-pointer-comparison
  • Add built-in operators for lists in ACSL
  • Add notation { x, y, z } for defining sets in ACSL
  • do not crash when loading statuses depending from non existing parameter.
  • Option -collect-messages is obsolete and will be removed in a future version; messages are now always collected.
  • Introduced a built-in for printing all sub-expressions of an expression (with their values). The built-in is called “tis_print_subexps” and takes a constant description string followed by any number of expressions as arguments. It is also used to show information when the “The following sub-expression cannot be evaluated (…)” warning happens.

Tis Analyzer++

  • Support the use of constexpr.
  • Supports now the use of contracts in templated functions and members in templated classes.
  • Add correct behavior to class member of reference type.

Release 1.19

Tis Analyzer

  • Avoid comment duplications on generated code.
  • Comments are preserved even when loops are unrolled.
  • Option -warn-undeclared-callee changed to implicit-function-declaration, which receives an argument (ignore, warn or error) specifying what to do when an undeclared function is called.
  • The untyped AST is no longer removed by basic program transformations such as loop unrolling
  • Fix clearing of old statuses and hypotheses when a new status is emitted or an annotation is removed.
  • Fix crash in tis_memcmp on very imprecise input.
  • Fix order of lemmas in Why3 output.

Tis Analyzer++

  • Support initialization of members in the implicit default constructor.
  • Local enums are now supported.
  • Fixes support of chained cases in a switch
  • added scalar initialization with single-element lists
  • Fixes support for switch with an empty body Support for range in case labels
  • Support packing pragmas
  • Use of ACSL annotation is possible in function templates
  • global variables can now be used on multiple files
  • Add the possibility to use __builtin_offsetof

Release 1.18

Tis Analyzer

Improvements

  • Documentation: a Quick Start guide with step-by-step tutorials and videos has been added to the documentation
  • Add a column to the information about the functions to tell whether they are static.

Release 1.17

GUI (beta)

Improvements

  • Grids:
    • Generated CSV files no longer contain the “ID” field if this field is not shown in the GUI.
    • “Files” columns have now also the line number in addition of the file’s name (except for the Functions grid)
  • Callstacks: Add an option (in the Option panel) to display callstacks with prettified filepaths
  • Interface: A scroller has been added to panels’ toolbars when the toolbar’s content is larger than the panel’s width
  • Interactive code: When Value is computed, the body of functions that are mapped to a built-in of the analyzer are now hidden and replaced by the built-in name

Bug fixes

  • Wigdets: Hidden detached widgets now stay hidden after a browser page reload
  • Remote grids: Data in remote grids are now computed only when the grid is visible
  • Focused callstack: Fix a bug on clicking on a call site when the focused callstack was too long
  • Value messages: Fix a bug when a sorting or filtering action is performed on this grid
  • Evaluate ACSL: Fix a bug on displaying some arrays of char
  • tis-occurences: doesn’t crash with some ill-formed terms but always displays an error message

New features

  • Statements: add columns about dead code blocks (id, entry point, exit point)

Tis Analyzer

  • New option: -tis-info-dead-blocks
  • New tool: tis-info-coverage helps to find dead statements when several analyses are involved (see tis-info documentation for more information).
  • Add new suffix ‘.ci’ for pre-processed files containing ACSL annotations to be pre-processed
  • New option -custom-annot-char for changing the character introducing ACSL annotations (instead of ‘@’)
  • During the evaluation of ACSL ‘assert’, intermediate statuses (e.g. True, then Unknown, then True) are now reported in the console
  • Add support for parsing digraphs
  • Fix stack overflow with large range in case labels. Also fix unsoundness with dataflow analysis on programs containing multiple overlapping case labels.
  • Better precision for calls through function pointers when multiple functions are possible. The abstract state now contains the information of which function was called.
  • Double pointer casts on the NULL pointer are now simplified
  • Typing within comparisons is now more strict, or made more explicit through casts.
  • Corrected the getopt related headers (fixed an issue in unistd.h, which was defining identifiers that it was not supposed to though over-inclusion), added the INADDR_LOOPBACK constant in the netinet/in.h header file.
  • Improved the interpreter mode: changed behavior on some errors,
  • added options for handling the main function arguments through the command line (with new parameters “-val-args” and “-val-program-name”).
  • fix bug on some complex for loops
  • New alarm “division overflow” for INT_MIN / (-1) and INT_MIN % (-1)
  • the read variables set is now correctly computed for arrays and structs.
  • __builtin_constant_p and sizeof can now be used with complex expressions.
  • Add tis_asprintf_interpreter builtin (only for use in interpreter mode).
  • Add tis_memchr builtin
  • Fixed bug in tis_snprintf. The function now correctly returns the size that would have been written if n had been large enough, instead of the actual size written. tis_snprintf now treats also the case of a size argument which is a mix of addresses and integers (discarding the address part).
  • Add tis_memcpy builtin, which features detection of undefined behaviors caused by overlapping arguments. This builtin should replace the Frama_C_memcpy builtin.

Release 1.16

GUI (beta)

New features

  • Widgets: A new contextual menu has been added on widget titles in order to reset the targetted widget configuration to the default one
  • WP Goals: the WP plugin is now supported.
    • the WP plugin can be called on properties, function calls and function definitions
    • three options can be set from the GUI (-wp-timeout, -wp-split and-wp-model)
    • proof obligations are accessible for each WP result.

Tis Analyzer

  • Fix definition of INT64_C (resp. INTMAX_C) to be compatible with PRIi64 (resp. PRIiMAX) on 64-bit platforms, fix contributed by Brian Mastenbrook.
  • Fix bug in tis_variable_split builtin when applied to const variable.

Release 1.15

GUI (beta)

Improvements

  • Widgets:
    • When a widget is detached, the size of the created window is now the size of the widget itself before been detached
    • Widgets are now more visible when they are moved or reattached to the left side
  • Interactive code: A tooltip has been added on temporary variables to show the substituted expression
  • Source code: Colors used for the highlighting now match the interactive code ones

Bug fixes

  • Interactive code: Clicking on a “instance of requires” property in the Properties panel now highlight correctly the statement where the property is
  • Statements: in the “Join reason” column’s filter, the “” option is now displayed correctly

Find Occurrence

  • Support for queries on very large numerical addresses on the commandline

Tis Analyzer

  • Assertions containing \at(P, L), where L is a C label, can now be evaluated. Evaluation is done once Value has run; thus, it ignores option -slevel
  • pointer_comparable alarms are now emitted with arguments properly cast to void* or void (*)()
  • The alarms raised when evaluating a global initializer that leads to an undefined behavior are now marked with an “Invalid” status
  • Reports in csv format now honor option report-specialized (previously, preconditions at a callsite were always skipped)
  • Fix bug in the specifications of readir, opendir, closedir and fopen functions, that would cause incorrect analysis in -lib-entry-mode
  • WIDEN_HINTS directive are now cumulative with automatically inferred bounds.
  • Fix bug related to nested initialisations of structures containing pointers
  • All plugins that depend on Value, plus Value itself are now dynamic. Custom plugins must specify in their Makefile the plugins they depend on (e.g. PLUGIN_DEPENDENCIES:=Inout Value)
  • Cil transformation can introduce assertion to ensure that size expressions in an array declarations evaluated at program execution time are positive and do not overflow.
  • Garbled mix origins now include at most one source location
  • New option -report-proven to control the display of proven properties
  • New export format (.csv), through option -report-csv
  • Float operations that are guaranteed to lead to +/-infty (e.g. x = FLT_MAX*10.) now stop propagation. Previous behavior was to continue with an imprecise value for x.
  • Added built-ins for mathematical functions atan2, fmod, pow, expf, logf, log10f, powf, sqrtf.
  • Added built-ins for mathematical functions: atan2, fmod, pow, expf, logf, log10f, powf, sqrtf, floor, floorf, ceil, ceilf, round, roundf, trunc, truncf.

Release 1.14

GUI (beta)

Improvements

  • History: the back and forward buttons now takes in consideration the focused callstack.
  • Grids: Tooltips have been added for columns’ title and filters’ button
  • State Explorer: the “” value should now be correctly displayed
  • Interactive code: the blink animation has been removed

tis-analyzer

  • New option: -tis-info-compute
  • New watchpoint type for garbled mix. Register one with e.g. tis_watch_garbled(&ptr_lv, sizeof ptr_lv, 1);
  • Pure expressions ‘e;’ in statments position are no longer normalized into an if statement but into ‘T tmp = e;’. Non initialization alarms are hence no longer emitted.
  • Concurrent analyses using Mthread plugin are more precise

Release 1.13

tis-analyzer

  • New option: -volatile-globals
  • Add a builtin for strchr
  • Check for valid pointers on call of some builtins (mem* and strn*) when given size is 0. Display warnings when an undefined behavior is detected.
  • The tis_printf builtin now supports a wider range of format specifiers and flags as well as asterisk in the width and length fields. Format support for integer, string and double conversion specifiers should be exhaustive now.
  • Option -val-split-return-auto now always split between NULL/non-NULL pointers
  • The semantics of copying a lvalue has been changed when a type mismatch occurs between the destination and the copied value. A bitwise reinterpretation of the value to the destination type is now performed during the copy.
  • Check the validity of the operands of the ACSL operators /, %, << and >> when evaluating a predicate
  • Better typing of ‘?’ operator.
  • Do not emit pointer_comparable alarms on valid pointer comparisons involving objects of size 0
  • Pointer comparisons using relational operators (<, >=, etc) between a pointer and NULL is now flagged as undefined.
  • Fix typing bug when converting into a term an expression containing a pointer substraction
  • Functions call using a function pointer are now treated more leniently when too many arguments are supplied. An alarm is emitted, but execution continues with the right number of arguments.

GUI (beta)

New Features

  • The “List of widgets” button has been added in the toolbar and allow the user to show or hide widgets
  • New widgets: “Files”, “Types” and “Variables”. These widgets gather information about the source files, the types and the variables of the analyzed program. These information can also be obtained with the “-tis-info-files”, “-tis-info-types” and “-tis-info-variables” option.
  • A “Back” and “Forward” button has been added in order to keep an history on the interactive code tabs. Keyboard shortcuts “Alt-” and “Alt-” are bound to these button. The browser “Back” button has been disable to avoid some misfortunes.

Improvements

  • Server: TIS-Analyzer will now wait for user input if the port number is already in use. The user may press Enter to retry or input another port number.
  • Slicing: the slicing feature has now its own panel and allow to
    • Switch easily between several slicing projects
    • Export a slicing request into a Frama-C project
    • Download the sliced program from a slicing project
  • Evaluate ACSL Terms: terms are now saved and restored on Frama-C current project changes
  • Interactive code:
    • Alarm annotations, Degeneration points and Unpropagated statements are now “callstack wise”
    • Global tabs are now saved and restored across different sessions (even after restarting the server) and only globals tabs that are relevant in the new TIS-Analyzer instance are kept
  • Remote grids: several grids are now on the server side and only data visible in the browser will be downloaded from the TIS-Analyzer Server.
    • The “Compute” button has been removed: remote grids are loaded when grids are shown
    • The “Download” button now appears for every remote grid
    • CSV files obtained with “Download” now take in consideration active filters. The “Download” button has a visual feedback when at least one filter is active.
    • The following widgets now use a remote grid: “Globals”, “Functions”, “Statements”, “Properties”, “State Explorer”, “Value Messages”, “Find Occurrence” and “Shared Variables”
  • Grids: String filters now allows only POSIX regular expression. A button has been added to either match or to not match the given string.
  • State Explorer:
    • a visual feedback has been added when no term has been selected or when no result has been found
    • a new column with after states is now available for assignments and calls
  • Value Messages: small display improvements
  • Callstacks: the callstack grid has been reworked:
    • A new column has been added for the callstack’s function
    • Favorite callstacks are no longer duplicated
    • The grid can now be sorted by the favorite column, which will put at top/bottom the favorite callstacks except the one of the current function
  • Function context:
    • In a context, callsites that appear with the status “Syntactic” and “Semantic” are now shown as a single line with the status “Both”
    • The status is now callstack-wise and depends on the focused callstack
    • Add a filter to show only once the functions in the context (this will hide the different callsites in the grid)
  • Statement context:
    • the ID column has been replaced by a Information column
    • Occurrence statements have now the information about if the statement read the variable or wrote it
  • Documentation: Help boxes have been added for each GUI Widget and can be shown/hidden from the Option panel.
  • Callgraph: Improve performances and ergonomy
    • Controls has been reworked:
      • Simple left-click: select a node/edge
      • Double left-click: show the node’s children
      • Simple right-click: open the contextual menu
    • Coloring nodes by a property is now more relevant:
      • Green/Red for boolean property (respectively for yes/no)
      • A color gradient for others properties
  • Closable tabs can now also be closed with the middle click (with the wheel button)
  • Source code: on selecting a line in the source code, if this line can have several locations in different globals, a window will appear to let the user pick the location he wants to see. This behavior can easily occurs on analyzing a C++ code.

Bug fixes

  • Several bugs have been fixed in the feature that allow to move and detach panels
  • The pulsed-blue selection appears wrongly sometimes on visiting a global the first time in the interactive code panel
  • The hiliting of the interactive code is now correctly reset on expanding/reducing the focused callstack with the contextual menu
  • The program point cursor should now be correctly placed in functions where an alarm has been filtered by the focused callstack
  • Bugs related to large data grids has been fixed with the new Remote grids
  • The “Value Messages” widget’s data are now correctly saved after a ‘-save’
  • Fix a bug where some litteral strings in the interactive code was interpreted as HTML
  • In the interactive code, tabs order are now saved and restored correctly after refreshing the browser page
  • Occurrences in dead code are no longer wrongly-highlighted
  • The line shown in the source code is now also synchronized when the current tab in the interactive code is changed. The line shown is now the global one or the current program point if this point is in the current tab.

Release 1.12

GUI (beta)

New Features

  • Clipboard: A new entry in the contextual menu appear on some data and will allow you to copy this data into your clipboard (for pasting it anywhere). Concerned data are:
    • grid cells (useful for copy/paste values into a filter)
    • the focused callstack
    • some tabs (global names in the interactive code and filenames in the source code)
  • In the interactive code:
    • A new entry “Track term” has been added in the contextual menu on terms
    • A shortcut is now available for tracking terms: Ctrl + left click
    • A shortcut for expanding and reducing the focused callstack is available in the contextual menu on relevant functions related to the focused callstack
  • Panels position are now more configurable by right-clicking on their title:
    • All tabs and panels on the left side are now detachable
    • Panels on the left side can be reordered
    • Panels on the left side can be moved into the bottom side and vice versa

Improvements

  • Flamegraph statistics are now simpler: only functions are shown.
  • The exactness of the slevel information is improved.
  • The exactness of the State explorer tab is improved.
  • Remove google-code-prettify dependencies. The syntactic highlighting is now done by TIS-Analyzer
  • In the interactive code:
    • ACSL keywords have their own color
    • The “goto” selection (pulsed blue) and the “mouse” selection (green) have been merged into one unique selection (pulsed blue)
    • Types without definition are no longer clickable.
    • The current program point is now correctly synchronized with the pulsed-blue selection
    • For a ‘struct’ or ‘typedef’ definition, all other dependent type definitions are now printed below the current definition
  • In Evaluate ACSL Terms:
    • Description texts now replace empty texts that are sometimes shown in columns “Before” and “After”
    • The current term is now synchronized with the pulsed-blue selection, and unset when the selection is not a term in order to avoid misunderstandings
    • On clickable left-values in “Before” and “After” columns, if the clicked left-value is a function, the GUI will show this function in the interactive code instead of changing the current term in Evaluate ACSL Terms.
  • On using the “-load” option, the filename given to this option is now shown in the browser page title
  • For callstacks, it’s now possible to choose the call site additionnal number in the following choices (Note: the call site additionnal number is the number printed after the “@” in callstacks) :
    • the statement ID (default in 1.11 and previous versions),
    • the statement number inside its function
    • the statement location in the source files
  • The properties status in the Properties tab are now as precise as bullets in the interactive code.
  • Clicking in a source file in the “Source code” panel will now show the associated line in the normalized code in the interactive code panel. See documentation for exceptions.
  • For the interactive code panels and source code panels, all tabs or all other tabs than the one selected can be closed by right-clicking on the tab name.

Bug fixes

  • In grids, clicking on a row which is already selected should now correctly fire the click action
  • Find occurrence Plug-in errors are now correctly catched and displayed as warnings in the GUI.
  • Problems during the window resizing have been corrected
  • Status (position, size, …) of the different GUI components are now correctly saved and restored through sessions and browser reloads.
  • The “Save/Load Config” buttons feature is now restored and supported by more browsers. Configurations saved in this version of TIS-Analyzer should also be restored for future versions of TIS-Analyzer (except if the compatibility is deliberately broken and notified in the CHANGELOG)
  • Fix a bug when clicking on some statements in the panel like “Current Statement” raised a server error.

TIS Analyzer

  • more columns in -tis-info-functions and -tis-info-statements.
  • split the property Status column into Status + MoreInfo and give a more precise status. The MoreInfo column is kept for compatibility since the provided information is available in other tables.
  • add the -tis-info-files option.
  • add the -tis-info-exit-status option.
  • add -val-slevel-results by default (enables State Explorer)
  • add tis_alloc_size builtin (available in tis_builtin.h)
  • rename and extend the libc runtime
  • passing program options to tis-mk-main is now possible.
  • In -lib-entry mode, allow the generation of initial states with 0-sized bitfields
  • Improved reduction by predicate \initialized when the argument is a range of locations
  • Assertions previously removed by remove-redundant-alarms are now marked as proven, but remain in the AST
  • Fix parsing of packing directives of the form ‘#pragma pack(push, N)’
  • In -lib-entry mode, functions pointers no longer force the generation of dummy functions. Instead, they are initialized to NULL.
  • In Metrics plugin, new category ‘Extern global variables’, that can be used to check whether some files are missing
  • In Metrics plugin, functions from Frama-C standard library are now hidden by default
  • Switch statements in which some cases are not constant expressions are now completely disallowed, as per the C standard.
  • Parsing no longer accepts structures containing incomplete types.
  • Special functions CEA_ have been removed
  • New ACSL predicate \valid_read_string in share/libc/__fc_string_axiomatic.h
  • Terms involving l-values that are bit-fields are now correctly handled
  • Fix incorrect simplifications of ‘!E’ to 0 when E is either an enum with value 0, or an expression whose value wraps.

Release 1.11

GUI (beta)

New Features

  • View per callstack: [experimental] too many callstacks? It’s now possible to focus a callstack and filter all others that are concerned by the focus one. The features impacted by this view per callstack are :
    • The semantic highlighting of the interactive code
    • Data in “Evaluate ACSL Term”
    • Data in “State explorer”

Improvements

  • Evaluate ACSL Terms panel is now more precise on some tracked terms
  • The Find occurrence plug-in has now filters and a counter for the number of occurrences

Bug fixes

  • The “Current Fonction” is now always refreshed correctly
  • Callstacks which contains only the entry point of the program now display a text instead of nothing
  • State Explorer used to Stack Overflow due to a js_of_ocaml bug. An id field has been added to solve this problem and restore the order (the id field should be sorted in reverse order)
  • Some locations of “garbled mix” origin wasn’t displayed correctly in “Evaluate ACSL Term” panel

Tis-mk-main

  • tis-mk-main is a new tool to generate a function that calls the main function to analyze with specified arguments. Documentation can be found in the manuals.

TIS Analyzer

  • Macro FRAMAC is defined when pre-processing C files in Frama-C
  • Fix bug in -memexec-all option in presence of instructions where evaluation was guaranteed to fail
  • Inputs of an instruction whose evaluation always fail include the sub-expressions for which evaluation succeeds
  • Added -no-tty option to disable terminal capabilities
  • Faster treatment of imprecise struct copying and left shifts in the logic
  • In synthetic results, for local variables that are not those of the current function, the approximated values encompass only the callstacks for which the variables were in scope in one of the callers
  • Local variables that are in scope but not yet initialized are now present in the environment
  • Option -subdivide-float-var has been renamed into val-subdivide-non-linear, and has now an effect on non-linear integer expressions

Release 1.10

GUI (beta)

New Features

  • State explorer: this new tab will help you to explore term values for all Value Plugin’s states. This tab will appeared only when the -val-slevel-results option is set
  • Value messages: a new tab has appeared which keep and show all messages emitted during the Value analysis (enabled with the option -value-messages)
  • Add a Statistics button to show a FlameGraph view of analysis time with respect to functions and statements callstacks.
  • The TIS-Analyzer documentation is now available from the GUI

Improvements

  • The left panel has been redesigned
  • Semantic callees are now shown in Function Context panels

Bug fixes

  • Fix filter for the column “Is in stdlib” in the globals grid
  • The slicing now appears in the GUI when it’s computed thanks to the command line options
  • Fix the bug when the GUI can crash on changing project
  • All actions that highlight something in the normalize code will now scroll to the correct line in the source code too

TIS Analyzer

  • Fix -tis-info-properties when no server is launched
  • Fix incoherent data when the current project is changed
  • Add two builtins: strcmp and strnlen
  • Add a -val-statistics option (enabled by default, disable with -no-val-statistics) to measure value performance
  • Add Mthread to the tis-analyzer script
  • Improvements to option -subdivide-float-var, when subdividing may avoid the emission of an alarm
  • Support for \subset predicate in Value
  • Special functions CEA_ are deprecated. Use Frama_C_show_each or Frama_C_dump_each instead.
  • Improve pretty-printing of some loops.
  • -load-module M now works fine if M uses the API of another plug-in.
  • Option -pp-annot should be much faster when parsing files with many ACSL annotations.

Release 1.9

GUI (beta)

New Features

  • Multi-users: Several users on the same server are now allowed
    • Explore the same software as your workmates without disturbing them (except if you change the Frama-C project or launch the Value analysis, but they will be warned if you do this!)
    • Broadcast messages to all other users of this server
    • Share a position in the normalized code with the new contextual menu “Create link”
  • [experimental] Find occurrence plug-in is now supported in the GUI
  • The “Options” panel is now available in the top menu bar: the GUI will be more and more customizable in a near future
  • Add a “Shared variables” tab to show possible read/write data races detected by Mthread (relevant only if using Mthread plugin)

Improvements

  • In statements tab, show “N/A” instead of -1 for the slevel ratio when the slevel is zero, and show “N/A” instead of 0 for the slevel of unreachable statements.
  • Show when a statement is non terminating in some callstacks with a red dashed vertical line. The red plain vertical line is still used for statements non terminating in all callstacks.
  • Occurrence and Show defs results can be cleared
  • Show statement and function statistics about analysis time.
  • Some improvement for:
    • the normalized code panel
    • the normalized code highlighting
    • the Evaluate ACSL Terms for large values
  • The title of the browser page can now be choosen with the option “-server-name”
  • Large source files can now be displayed on demand
  • In Evaluate ACSL Terms, terms that are not lvalues and initial states are also shown in a per callstack manner
  • For CSV files, the CSV separator and the floating number separator can be chosen in the Options panel (allow to switch in french CSV mode)
  • For grids with filters, a “Reset Filters” button has been added
  • For grids with filters, the button text of “select” filter type adjust itseft according to the selected choice
  • The GUI clears automatically cached data when a TIS-Analyzer update is detected

Bug fixes

  • Fix slicing display problems
  • Fix display of the “goto” marker (marker which is display when an action send the user to a location in the normalized code) with Firefox
  • Clicking in properties/functions panels no longer raises errors
  • Fix problems with CSV files

tis-analyzer script

  • Change default Frama-C options:
    • Add -permissive
    • Remove -val-after-results (always ON in Frama-C)
  • Add a -load option (e.g. tis-analyzer-gui -load state)
  • Add a -help option

TIS Analyzer

  • The ACSL parser now ignores /@{ and /@} comments, to avoid conflicting with Doxygen
  • Accesses to locations that contain garbled mix now cause the garbled mix to be reduced to the set of valid locations
  • Add -tis-print-deps to print the dependencies of lval at the end of the entry point.
  • Add -tis-occurrence to list all statements that may access lval.
  • Accesses to *(foo *)p may now reduce p according to the validity of the access, when useful
  • Removed message “assigning non-deterministic value from the first time”
  • New option -val-initialization-padding-globals to specify how padding bits should be initialized. Option -initialized-padding-globals is deprecated
  • Fix initial state in which some volatile or const qualifiers for nested types were ignored
  • Fix incorrect initialization of padding bits. Option initialized-padding was ignored in some cases
  • Fix generation of initial memory state in presence of C99 designated initializers

Release 1.8

GUI (beta)

Bug Fixes

  • Now works under Firefox
  • In Evaluate ACSL Terms, data in callstacks are now refreshed correctly
  • Properties and Functions grids are cleared properly when the server’s session changes
  • Dashboard’s summary texts now display the right informations

New features

  • Add more informations in Functions and Statements grids
  • Grids data can now be downloaded as a CSV file
  • Slicing is now available on left-values and statements (experimental).

Frama-C

  • Option -slevel-merge-after-loop renamed to val-slevel-merge-after-loop. Now takes a set of kernel functions as an argument.
  • Per-callstack results are now always computed. Option -val-callstack-results is deprecated.

Release 1.7

  • improve documentation of tis-analyzer
  • increase precision of analysis
  • new GUI (beta release): see README on the desktop
  • improve tis-make and tis-mkfs
  • new license management system