infer_clone

Commit Graph

Author	SHA1	Message	Date
Jules Villard	4f77f82cba	[pulse] some models should "prune" instead of "and" Summary: Instead of recording some facts as "known" (i.e., observed assignments), record them as "pruned". This should be done any time the fact is not an assignment, for instance when path-splitting on "is the argument =0?" as in the model of `free()`. Reviewed By: ezgicicek Differential Revision: D26450362 fbshipit-source-id: 4fc980f90	4 years ago
Gabriela Cunha Sampaio	be39e74bd4	[pulse] Modeling checkState and checkArgument Summary: providing models for the checkState and checkArgument functions, both used in Java code. Reviewed By: da319 Differential Revision: D26101726 fbshipit-source-id: 0cc73d252	4 years ago

Author

SHA1

Message

Date

Jules Villard

4f77f82cba

[pulse] some models should "prune" instead of "and"

Summary:
Instead of recording some facts as "known" (i.e., observed assignments),
record them as "pruned". This should be done any time the fact is not an
assignment, for instance when path-splitting on "is the argument =0?" as
in the model of `free()`.

Reviewed By: ezgicicek

Differential Revision: D26450362

fbshipit-source-id: 4fc980f90

Gabriela Cunha Sampaio

be39e74bd4

[pulse] Modeling checkState and checkArgument

Summary:
providing models for the checkState and checkArgument
functions, both used in Java code.

Reviewed By: da319

Differential Revision: D26101726

fbshipit-source-id: 0cc73d252

2 Commits (e98fe8d24c46f617bc66cf404db81be1c2da5339)