Input:programs/regression/c/BugForLoop01.c
Settings:settings/automizer/TreeInterpolants.epf
Toolchain:toolchains/AutomizerC.xml

fails as follows

NullPointerException: null: de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.CACSL2BoogieBacktranslator$CheckForSubtreeInclusion.check(CACSL2BoogieBacktranslator.java:819)

Currently, our termination analysis analyzes all loops of a program. It would be better if we could specify which loop should be analyzed.

More precisely, which location may not appear infinitely often.
This could be achieved with something like
//@assert isFinite() or __VERIFIER_assert_isFinite()

Write a fresh Ultimate plugin which takes a smtlib-file which uses "set-logic HORN" and builds the Horn Clause graph from it.
See also
https://github.com/ultimate-pa/ultimate/wiki/Tree-Automizer

Subtasks

• Integrate smtlib-parser into Ultimate
• implement conversion to a hyper graph
  • edges are labelled with a variant of TransitionFormula
  • nodes correspond to uninterpreted predicate symbols
    (..)

1 week
create a plugin "HornClauseGraphBuilder"
procedure right now:
copy an existing one, that is similar (RCFGBuilder), delete all code, except base classes (.. Activator, ~Observer, ~.java) rename in every place, also in plugin.xml
use smtlib2 parser from smtInterpol
alex: find out how to get the parser into ultimate
build the graph
alex: organize the graph base classes

Support all methods from string.h and from strings.h the following.

• int bcmp(const void *, const void *, size_t); /* LEGACY, see memcmp */
• void bcopy(const void *, void *, size_t); /* LEGACY, see memcpy, memmove */
• void bzero(void *, size_t); /* LEGACY, see memset */

For unit testing of some low-level implementations, it would be desirable to be able to create mock-ups of small data structures, such as a BoogieVar, without having to parse a whole Boogie program with a full Ultimate tool chain.

Currently, the creation process of a BoogieVar needs some SMT TermVariables, and ApplicationTerms which are not be available if one doesn't want to parse a whole Boogie program. Therefore, perform unit testing only on methods (without the whole Ultimate back-end) that require BoogieVars is impossible. For example, if a function that should be tested computes some values for which only the existence of BoogieVars is necessary, but the semantics of said BoogieVars is irrelevant, it would be nice to be able to create instances of BoogieVars which serve that purpose.

Additionally, it would also be nice to be able to create mock-ups of Boogie CodeBlocks from strings. E.g. by using "var x : int; x := 5", the CodeBlock data structure for those two statements is created (through parsing) to be able to test e.g. implementations that handle assignment operations.

We should be able to parse LTL properties from a separate file instead of only from comments in the C file or from our settings file

2Byte, 4 Byte, smallest signed first, smallest unsigned first, smallest signed only (additionally min/max number of bytes as boundaries)

This ticket depends on issue #42

• Use NOTICE log level in some places
• change log level configuration options for tools

I.e., not 0 but some non-deterministic value.

For building the webinterface, we the folder
trunk/source/Website/WebContent/json
is needed. Problem: Git does not support empty folders.
How should we fix this?

1. Add an auxiliary file in the folder.
2. Let convertHTMLtoJSON.jar create the folder.
3. ???

I'm on Ubuntu 14.04 (Gnome Shel 3.10.4)
I installed Eclipse CDT (Mars)
I installed ultimate according to the instructions

After importing the Projects, there are 57 errors in the Projects SpaceExParser, Website, WebstieEclipseBridge - see screenshot.

Assuming this is normal and not critical:

• This might confuse people (as it does me) when there are other problems with the installation process - I would strongly recommend adding that as a side note to the installation instruction page.

otherwise

• What is possibly missing/wrong with my installation?

Secondly the Create Run Configuration part failed.
After clicking "Launch an Eclipse application", the launch process fails.
error log on pastebin (Sadly github fails to accept the log file.)

Current work-around: Run ANT script manually

Expected solution: Run ANT script automatically :)

SIGINT should gracefully terminate the currently running toolchain (i.e., raise toolchaincanceled)

If I use the GUI to load the attached setting (has to append .txt to be able to upload it) Ultimate says

Loading preferences was successful

however, none of the changed options is used.
SmtInterpol_Craig_Conservative.epf.txt

Tests are smt2 scripts, right now (maybe something else later)

Things to test:
Parser part:

• is the full horn clause grammar in SMTLib recognized? (as specified on the sv-comp horn clause page referenced in the wiki?)
• is the right set of HornClauses extracted?
  Graph builder part:
  • is the hypergraph built correctly?

(might be extended -- what else to test?)

• currently, --experimental shows all options, non-experimental shows only options with description
• in the future non-experimental should only show options that are marked as visible in the toolchain file

As the title suggests: We want to be able to check for unsigned overflows.

Currently, when the SVComp benchmarks should be used for testing (e.g. with maven), one needs to take a look into trunk/examples/externalRepositories.txt for instructions on how to add the SVComp repository to the examples directory.

This process should be documented in the Wiki as well.

(relevance &(char*), var names)

Write some .ats test files that test the operations we have.

Use the assert statement from AutomataScript to indicate if the test fails or not.

Currently, the Ultimate-Wiki page https://github.com/ultimate-pa/ultimate/wiki/AddDeveloper is outdated. This page needs to be revised and altered to reflect the current state Ultimate's repositories.

As seen in Jan Hättig's presentation today, the result notifier states that there is no result when the real result is actually safe. Either remove the result notifier or fix this contradiction.

Eclipse 4 creates by default .gitignore in most directories to avoid tracking the /bin subdirectories. Shouldn't those be commited to the repository anyway? How do you handle them otherwise?

In certain situations, pointers can be completely resolved by duplicating functions. If this allows the removal of all pointers of a program, it can improve our performance greatly.

Real-world code often uses pointers for stateless library functions, where this could be beneficial.

See GasCake02 vs GasCake02_Pointerless for an example.

AutomataScript

• add possibility to write Trees in AutomataScript

Operations

• add accept(..)

In some cases, Ultimate dies because the SMTSolver ran into a timeout. Currently, we convert this situation to an error, although it should be a timeout.

This behavior should be changed, possibly in Executor or Scriptor.

Example stack trace:

[2016-02-17 13:39:26,265 ERROR L194        ToolchainWalker]: The Plugin de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction has thrown an Exception!
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: line 15920 column 10: canceled
        at de.uni_freiburg.informatik.ultimate.smtsolver.external.Parser$Action$.CUP$do_action(Parser.java:1339)
        at de.uni_freiburg.informatik.ultimate.smtsolver.external.Parser.do_action(Parser.java:584)
        at java_cup.runtime.LRParser.parse(LRParser.java:419)
        at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.parse(Executor.java:204)
        at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.parseCheckSatResult(Executor.java:226)
        at de.uni_freiburg.informatik.ultimate.smtsolver.external.Scriptor.checkSat(Scriptor.java:222)
[...]

• In L906 decimalNumber_s32 occurs two times with different values
• In L910 is a \read(decimalNumber_s32) with a negative value, and afterwards decimalNumber_s32 with the same value

Make the LBE/SBE of this plugin usable as separate plugin

It would be nice if our test suites would allow the specification of additional settings that are applied after a baseline settings file is loaded.

examples/programs/abstractInterpretation/regression/recursive-wrong-prestate.bpl

// Wrong (not inductive) transition and/or state added by AI
// The second disjunct of the hierachical pre state is probably the reason.
//
// PreState: (and (= foo_bla 0) (= foo_res 0))
// HierachicalPreState (or (<= 1 foo_bla) (<= (+ foo_bla 1) 0))
// Trans: return;
// Post: (and (= foo_res 0) (<= 1 foo_bla))

Currently, the value part of our error paths does not mention the scope of the variables. This can lead to complicated situations were users cannot distinguish between masked variables.

Possible solution:

• mark global variables as global
• prefix variable names with their scope, e.g. ::::::::

It would be beneficial to allow additional specifications:

• Global assertions (semantics as in LTL formula []P)
• Global assumptions (fix initial value of global or static variable to something different than 0 or *, add assume to havoc for volatile variables )

The backtranslation uses wrong variable names in the FailurePath's states.

For example boogiePrinter.zip(analyzed with AutomizerBPL toolchain):
[...,c=1, c=1, ...
should be something like
[..., pc0 = 1, pc1 = 1, ... .

The new CLI controller fails if there are options before the toolchain argument, because the toolchain help parser runs before and is not aware of those options.

We are unsound for the following input.

Program:programs/regression/c/Switch02.c 
Settings:settings/automizer/ForwardPredicates.epf 
Toolchain:toolchains/AutomizerC.xml

Presumed problem: In contradicion to the C standard, the controlling expression is converted to int.

• Tricore EABI Section 2.1.2
  http://www.infineon.com/dgdl/TriCore_EABI_v2_3.pdf?fileId=db3a304412b407950112b40f8d7a142b
• C166 EABI Section 2.6.2
  http://www.infineon.com/dgdl/c166sv2um.pdf?fileId=db3a304412b407950112b41d4ea32fe3
• MPC55xx Chapter 3
  http://refspecs.linux-foundation.org/elf/elfspec_ppc.pdf
  Extension of chapter 3
  http://www.nxp.com/files/32bit/doc/app_note/PPCEABI.pdf

Support the following functions from stdio.h.

• sprintf
• sscanf
• fprintf
• fscanf
• fopen
• freopen
• fflush
• fclose
• setbuf
• setvbuf
• fwide
• fread
• fwrite
• ftell
• fgetpos
• fseek
• fsetpos
• rewind
• remove
• rename
• tmpfile
• tmpnam

Missing requirement: de.uni_freiburg.informatik.ultimate.plugins.spaceex.parser 0.0.1 requires 'package de.uni_freiburg.informatik.ultimate.test 0.0.0' but it could not be found

LTL2Aut should support more / other LTL to Büchi tools (or, even better, an own Java implementation based on (maintained) libraries )

see logfile

We want to specify at which location an LTL step is allowed to take place. We can do this with ghost variables, but a designated specification can be used during product construction to drastically reduce the size of the product.