search

ApproxSymate / klee

KLEE Symbolic Virtual Machine for Numerical Precision Analysis
Other
0 stars 0 forks source link

Mark error that is computed via assuming floating point as int #14

Open domainexpert opened 7 years ago

domainexpert commented 7 years ago

This is to make it clear if approximation has been done.

domainexpert commented 7 years ago

As previously mentioned in #10, sterbenz.c of fp-examples may be a useful example, where there are branchings that are dependent on symbolic values.

Himeshi commented 6 years ago

@domainexpert What needs to be done here?

domainexpert commented 6 years ago

@Himeshi This was requested by Weng Fai some while ago. I believe this entails counting of floating-point instructions executed along the path (e.g., FAdd). In the current implementation, the floating-point instructions are made to have integral semantics, so this is an approximation. The count will indicate the severity of the approximation.

domainexpert commented 6 years ago

@Himeshi Please feel free to assign yourself this task if you want to work on it. I think it's not difficult.