You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The current implementation works for toy programs but two main things
must to be done for being able to analyze real programs:
landmarks must be kept as local state as part of each abstract
state.
reduction between scalar and weight domains must be done
incrementally. For that, we need some assumptions about the
underlying scalar domain. For instance, if we assume zones then
after each operation we know which are the indexes affected by
the operation. We can use that information for doing reduction
only on those indexes. This would remove the need of having
methods such as array_sgraph_domain_traits::is_unsat and array_sgraph_domain_traits::active_variables which are anyway
domain dependent.
Copied from original issue: caballa/crab#15
The text was updated successfully, but these errors were encountered:
From @caballa on April 9, 2017 8:34
The current implementation works for toy programs but two main things
must to be done for being able to analyze real programs:
landmarks must be kept as local state as part of each abstract
state.
reduction between scalar and weight domains must be done
incrementally. For that, we need some assumptions about the
underlying scalar domain. For instance, if we assume zones then
after each operation we know which are the indexes affected by
the operation. We can use that information for doing reduction
only on those indexes. This would remove the need of having
methods such as
array_sgraph_domain_traits::is_unsat
andarray_sgraph_domain_traits::active_variables
which are anywaydomain dependent.
Copied from original issue: caballa/crab#15
The text was updated successfully, but these errors were encountered: