search

qqiangwu / cppsafe

Cpp lifetime safety profile static analyzer
MIT License
45 stars 1 forks source link

rocksdb: category inference for `std::tuple` #20

Open qqiangwu opened 7 months ago

qqiangwu commented 7 months ago 
std::tuple<std::optional<Slice>, std::optional<Slice>>
MaybeAddTimestampsToRange(const Slice* start, const Slice* end, size_t ts_sz,
                          std::string* start_with_ts, std::string* end_with_ts,
                          bool exclusive_end);

the following contracts are infered

/Users/wuqq/dev/rocksdb-main/db/db_impl/db_impl_compaction_flush.cc:1040:3: warning: pset(Pre(start)) = ((null), *start)
 1040 |   __lifetime_contracts(&MaybeAddTimestampsToRange);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Users/wuqq/dev/rocksdb-main/db/db_impl/db_impl_compaction_flush.cc:1040:3: warning: pset(Pre(*start)) = (**start)
 1040 |   __lifetime_contracts(&MaybeAddTimestampsToRange);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Users/wuqq/dev/rocksdb-main/db/db_impl/db_impl_compaction_flush.cc:1040:3: warning: pset(Pre(end)) = ((null), *end)
 1040 |   __lifetime_contracts(&MaybeAddTimestampsToRange);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Users/wuqq/dev/rocksdb-main/db/db_impl/db_impl_compaction_flush.cc:1040:3: warning: pset(Pre(*end)) = (**end)
 1040 |   __lifetime_contracts(&MaybeAddTimestampsToRange);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Users/wuqq/dev/rocksdb-main/db/db_impl/db_impl_compaction_flush.cc:1040:3: warning: pset(Pre(start_with_ts)) = ((null), *start_with_ts)
 1040 |   __lifetime_contracts(&MaybeAddTimestampsToRange);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Users/wuqq/dev/rocksdb-main/db/db_impl/db_impl_compaction_flush.cc:1040:3: warning: pset(Pre(*start_with_ts)) = (**start_with_ts)
 1040 |   __lifetime_contracts(&MaybeAddTimestampsToRange);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Users/wuqq/dev/rocksdb-main/db/db_impl/db_impl_compaction_flush.cc:1040:3: warning: pset(Pre(end_with_ts)) = ((null), *end_with_ts)
 1040 |   __lifetime_contracts(&MaybeAddTimestampsToRange);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Users/wuqq/dev/rocksdb-main/db/db_impl/db_impl_compaction_flush.cc:1040:3: warning: pset(Pre(*end_with_ts)) = (**end_with_ts)
 1040 |   __lifetime_contracts(&MaybeAddTimestampsToRange);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

No postconditions are derived.