File tree 2 files changed +15
-3
lines changed
2 files changed +15
-3
lines changed Original file line number Diff line number Diff line change @@ -1733,6 +1733,19 @@ void taint_summarise_all_functions(
1733
1733
1734
1734
auto start_time=std::chrono::high_resolution_clock::now ();
1735
1735
1736
+ // In the map 'lvsadb_flush_ref_counts' there we store for each function
1737
+ // in the inverted topological order two information:
1738
+ // - reference count (how many callers the function has)
1739
+ // - names of the callees
1740
+ // where both information are considered w.r.t. the inverted topological
1741
+ // order. Namely, considered are only recursive calls to predecessors in the
1742
+ // topological order.
1743
+ // We use the map for unloading not needed LVSA summaries from the memory
1744
+ // (but they are saved on the disk). An LVSA summary of a given function
1745
+ // is not needed at a given position in the inverted topological order of
1746
+ // functions, if none of the remaining function (i.e. those after the position
1747
+ // in the order) is a caller of the given function w.r.t the inverted
1748
+ // topological order.
1736
1749
typedef std::pair<std::size_t , std::unordered_set<irep_idt>>
1737
1750
refcount_and_calleest;
1738
1751
std::unordered_map<irep_idt, refcount_and_calleest> lvsadb_flush_ref_counts;
@@ -1845,7 +1858,6 @@ void taint_summarise_all_functions(
1845
1858
--elem.first ;
1846
1859
if (elem.first == 0UL )
1847
1860
{
1848
- std::cout << " @@@ Trying to flush: " << succ << std::endl;
1849
1861
const bool unloaded = lvsa_db.unload (succ);
1850
1862
INVARIANT (unloaded || skipped.count (succ) != 0UL ,
1851
1863
" Either the LVSA summary was unloaded or there was "
Original file line number Diff line number Diff line change @@ -514,10 +514,10 @@ class cached_mapt final
514
514
Function: cached_mapt::unload(const key_type &)
515
515
516
516
Inputs:
517
- key: A key whose corresponding value should be unload .
517
+ key: A key whose corresponding value should be unloaded .
518
518
519
519
Outputs:
520
- True, if the referenced element was unload , and false otherwise.
520
+ True, if the referenced element was unloaded , and false otherwise.
521
521
522
522
Purpose:
523
523
Unloads the element referenced by the passed key in the cache to allow the
You can’t perform that action at this time.
0 commit comments